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.
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
Thank you @Quinn !
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