Callan McGill (Jan 24 2022 at 19:09): Callan McGill (Jan 24 2022 at 19:09):Could someone remind me of the typical way to write a lemma in the middle of a proof (the equivalent of have in Lean), I have been searching around but can't find the typical thing people do.
Karl Palmskog (Jan 24 2022 at 19:11):Coq has several proof/tactic languages that do this in different ways, I assume you mean plain Ltac: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.assert
Quinn (Jan 24 2022 at 19:11):assert
Callan McGill (Jan 24 2022 at 19:12):Thank you @Quinn !
Assia Mahboubi (Jan 25 2022 at 09:20):There is a have tactic in Coq as well, available as soon as you
Require Import ssreflect.
Toy examples of basic usage:
Require Import Psatz ssreflect.
Lemma example (n m : nat) : n <= 0 -> m <= n -> n * m = 0.
Proof.
intros le0n le0m.
have eqn0 : n = 0. (* basic *)
lia.
have foo (k : nat) : k + n = k by lia. (* the syntax is akin to that of the global Lemma command *)
have eqm0 : m = 0 by lia. (* ommit the dot is the proof is a one-liner *)
have -> : n * m = 0 by lia. (* in fact you can even use an intro pattern instead of the name for the local lemma, here to rewrite on the fly *)
lia.
Qed.
Last updated: Sep 23 2023 at 08:01 UTC