14.4. False sentences and fall-through🔗

The tactic constructs proofs only for true sentences. For a false universal sentence it identifies a cell on which the body is false:

example : ∀ x : ℝ, x ^ 2 > 0 := by⊢ ∀ (x : ℝ), x ^ 2 > 0
  rcf: the universal sentence is false on the root cell isolated in (-2, 2]rcf⊢ ∀ (x : ℝ), x ^ 2 > 0

rcf: the universal sentence is false on the root cell isolated in (-2, 2]

For a false existential sentence it reports that all relevant cells were checked and that none supplies a witness:

example : ∃ x : ℝ, x ^ 2 + 1 = 0 := by⊢ ∃ x, x ^ 2 + 1 = 0
  rcf: the existential sentence is false. Every relevant decomposition
cell was checked and found false, so there is no witnessrcf⊢ ∃ x, x ^ 2 + 1 = 0

rcf: the existential sentence is false. Every relevant decomposition
cell was checked and found false, so there is no witness

A sentence can be well formed and false. rcf then reports the failure shown above and produces no proof. A goal outside the fragment is different: it is not recognised as a sentence at all, and rcf fails before any computation. Both are ordinary tactic failures, so tactic combinators may fall through to another method. Here the unquantified goal is outside the fragment and norm_num handles it:

example : (0 : ℝ) < 1 := by⊢ 0 < 1
  first | rcf⊢ 0 < 1 | norm_numAll goals completed! 🐙