Stream: Coq users

Topic: intermediate goal in proof


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Quinn (Jan 24 2022 at 19:11):

assert

view this post on Zulip Callan McGill (Jan 24 2022 at 19:12):

Thank you @Quinn !

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC