How to write intermediate proof statements inside Coq - similar to how in Isar one has have Statement using Lemma1, Lemma2 by auto but in Coq?

Link:: https://stackoverflow.com/q/70324745

Display all goals and responses

Question

I wanted to write intermediate lemmas inside Coq proof scripts, e.g., inside SCRIPT in Proof. SCRIPT Qed. itself - similar to how one would do in Isar. How does one do this in Coq? e.g.:

have Lemma using Lemma1, Lemma2 by auto.

I am aware of the exact statement and wonder if that is it... but I'd like to have the proof for the statement too like in Isar we have have by auto or using Proof. LEMMA_PROOF Qed.

To make it concrete, I was trying to do these very simple proofs:

Module small_example.

Theorem add_easy_induct_1 : forall n : nat, n + 0 = n.forall n : nat, n + 0 = n
Proof.forall n : nat, n + 0 = n
  intros.n: nat
n + 0 = n induction n as [| n' IH].0 + 0 = 0
n': nat
IH: n' + 0 = n'
S n' + 0 = S n'
  -0 + 0 = 0 simpl.0 = 0 reflexivity.
  -n': nat
IH: n' + 0 = n'
S n' + 0 = S n' simpl.n': nat
IH: n' + 0 = n'
S (n' + 0) = S n' rewrite -> IH.n': nat
IH: n' + 0 = n'
S n' = S n' reflexivity.
Qed.

Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).forall n m : nat, S (n + m) = n + S m
Proof.forall n m : nat, S (n + m) = n + S m
  intros n m.n, m: nat
S (n + m) = n + S m induction n as [| n' IH].m: nat
S (0 + m) = 0 + S m
n', m: nat
IH: S (n' + m) = n' + S m
S (S n' + m) = S n' + S m
  -m: nat
S (0 + m) = 0 + S m simpl.m: nat
S m = S m reflexivity.
  -n', m: nat
IH: S (n' + m) = n' + S m
S (S n' + m) = S n' + S m simpl.n', m: nat
IH: S (n' + m) = n' + S m
S (S (n' + m)) = S (n' + S m) rewrite -> IH.n', m: nat
IH: S (n' + m) = n' + S m
S (n' + S m) = S (n' + S m) reflexivity.
Qed.

Theorem add_comm : forall n m : nat, n + m = m + n.forall n m : nat, n + m = m + n
Proof.forall n m : nat, n + m = m + n
  intros.n, m: nat
n + m = m + n induction n as [| n' IH].m: nat
0 + m = m + 0
n', m: nat
IH: n' + m = m + n'
S n' + m = m + S n'
  -m: nat
0 + m = m + 0 simpl.m: nat
m = m + 0 rewrite -> add_easy_induct_1.m: nat
m = m reflexivity.
  -n', m: nat
IH: n' + m = m + n'
S n' + m = m + S n' simpl.n', m: nat
IH: n' + m = m + n'
S (n' + m) = m + S n' rewrite -> IH.n', m: nat
IH: n' + m = m + n'
S (m + n') = m + S n' simpl.n', m: nat
IH: n' + m = m + n'
S (m + n') = m + S n' rewrite <- plus_n_Sm.n', m: nat
IH: n' + m = m + n'
S (m + n') = S (m + n') reflexivity.
Qed.

End small_example.

but I wasn't sure how and it wasn't working too well.

I'm also interested in shows in Coq e.g.

shows T using lemmas by hammer.

Current answers are good in showing that the have and by statements exist in Coq. However, what is crucially missing is 1) the shows statement and 2) the using statements. I'd like to see similar constructs with those in Coq proofs -- especially the using one that works with shows's and have's.

What Isabelle seems to be good at is declaring statements as true given a proof and a list of hypothesis. So for example have name: L using l1 by metis. would create the lemma L as a new fact, give it name name but prove it using the tactic metis but crucially depending on the fact l1 as something given for that statement to succeed. So I want to be able to declare things and be checked by a tactic/ATP in Coq.

I am aware of Czar (https://coq.discourse.group/t/what-is-the-difference-between-ssreflect-and-czar/824) but that is no longer supported in Coq afaik.

Answer (Li-yao Xia)

You can write assert <lem> to prove an intermediate result <lem> in the middle of a proof. Other variants are assert <lem> by <tactic> to immediately prove <lem> using <tactic>, or assert (<lemname> : <lem>) to give a name to the lemma. Example:

Theorem add_comm : forall n m : nat, n + m = m + n.forall n m : nat, n + m = m + n
Proof.forall n m : nat, n + m = m + n
  intros.n, m: nat
n + m = m + n induction n as [| n' IH].m: nat
0 + m = m + 0
n', m: nat
IH: n' + m = m + n'
S n' + m = m + S n'
  -m: nat
0 + m = m + 0 simpl.m: nat
m = m + 0
    assert (add_easy_induct_1 : forall n, n + 0 = n) by (induction n; auto).m: nat
add_easy_induct_1: forall n : nat, n + 0 = n
m = m + 0
    rewrite -> add_easy_induct_1.m: nat
add_easy_induct_1: forall n : nat, n + 0 = n
m = m reflexivity.
  -n', m: nat
IH: n' + m = m + n'
S n' + m = m + S n' simpl.n', m: nat
IH: n' + m = m + n'
S (n' + m) = m + S n'
    assert (plus_n_Sm : forall n m, S (n + m) = n + S m) by (induction n; auto).n', m: nat
IH: n' + m = m + n'
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
S (n' + m) = m + S n'
    rewrite -> IH.n', m: nat
IH: n' + m = m + n'
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
S (m + n') = m + S n' simpl.n', m: nat
IH: n' + m = m + n'
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
S (m + n') = m + S n' rewrite <- plus_n_Sm.n', m: nat
IH: n' + m = m + n'
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
S (m + n') = S (m + n') reflexivity.
Qed.

Documentation on assert: https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.assert

Answer (Pierre Jouvelot)

You can use the have: construct in the ssreflect language of tactics for Coq, with pretty much the same semantics you want, plus a couple of additional nice features related to how this lemma can be used right away (e.g., for rewriting) instead of being given a name.

For a concrete code example, see https://stackoverflow.com/a/71428239/1601580

Answer (Charlie Parker)

To provide an example to https://stackoverflow.com/a/70326508/1601580 answer, here is some code example for have:

Theorem n_plus_zero_eq_n : forall n : nat, n + 0 = n.forall n : nat, n + 0 = n
Proof.forall n : nat, n + 0 = n
  intros.n: nat
n + 0 = n induction n as [| n' IH].0 + 0 = 0
n': nat
IH: n' + 0 = n'
S n' + 0 = S n'
  -0 + 0 = 0 simpl.0 = 0 reflexivity.
  -n': nat
IH: n' + 0 = n'
S n' + 0 = S n' simpl.n': nat
IH: n' + 0 = n'
S (n' + 0) = S n' rewrite -> IH.n': nat
IH: n' + 0 = n'
S n' = S n' reflexivity.
Qed.

Theorem Sn_plus_m_eq_n_plus_Sm : forall n m : nat, S (n + m) = n + (S m).forall n m : nat, S (n + m) = n + S m
Proof.forall n m : nat, S (n + m) = n + S m
  intros n m.n, m: nat
S (n + m) = n + S m induction n as [| n' IH].m: nat
S (0 + m) = 0 + S m
n', m: nat
IH: S (n' + m) = n' + S m
S (S n' + m) = S n' + S m
  -m: nat
S (0 + m) = 0 + S m auto.
  -n', m: nat
IH: S (n' + m) = n' + S m
S (S n' + m) = S n' + S m simpl.n', m: nat
IH: S (n' + m) = n' + S m
S (S (n' + m)) = S (n' + S m) rewrite <- IH.n', m: nat
IH: S (n' + m) = n' + S m
S (S (n' + m)) = S (S (n' + m)) reflexivity.
Qed.

Theorem add_comm : forall n m : nat, n + m = m + n.forall n m : nat, n + m = m + n
Proof.forall n m : nat, n + m = m + n
  intros.n, m: nat
n + m = m + n induction n as [| n' IH].m: nat
0 + m = m + 0
n', m: nat
IH: n' + m = m + n'
S n' + m = m + S n'
  -m: nat
0 + m = m + 0 simpl.m: nat
m = m + 0 rewrite -> n_plus_zero_eq_n.m: nat
m = m reflexivity.
  -n', m: nat
IH: n' + m = m + n'
S n' + m = m + S n' simpl.n', m: nat
IH: n' + m = m + n'
S (n' + m) = m + S n' rewrite -> IH.n', m: nat
IH: n' + m = m + n'
S (m + n') = m + S n' rewrite -> Sn_plus_m_eq_n_plus_Sm.n', m: nat
IH: n' + m = m + n'
m + S n' = m + S n' reflexivity.
Qed.

(* have proof *)
From Coq Require Import ssreflect ssrfun ssrbool.

Theorem add_comm_have : forall n m : nat, n + m = m + n.forall n m : nat, n + m = m + n
Proof.forall n m : nat, n + m = m + n
  intros.n, m: nat
n + m = m + n induction n.m: nat
0 + m = m + 0
n, m: nat
IHn: n + m = m + n
S n + m = m + S n
  -m: nat
0 + m = m + 0 simpl.m: nat
m = m + 0
    have: (forall n, n + 0 = n) by apply n_plus_zero_eq_n.m: nat
(forall n : nat, n + 0 = n) -> m = m + 0
    move=> H.m: nat
H: forall n : nat, n + 0 = n
m = m + 0 rewrite -> H.m: nat
H: forall n : nat, n + 0 = n
m = m by reflexivity.
  -n, m: nat
IHn: n + m = m + n
S n + m = m + S n simpl.n, m: nat
IHn: n + m = m + n
S (n + m) = m + S n rewrite IHn.n, m: nat
IHn: n + m = m + n
S (m + n) = m + S n
    have: (forall n m : nat, S (n + m) = n + (S m))
      by apply Sn_plus_m_eq_n_plus_Sm.n, m: nat
IHn: n + m = m + n
(forall n m : nat, S (n + m) = n + S m) ->
S (m + n) = m + S n
    move=> H'.n, m: nat
IHn: n + m = m + n
H': forall n m : nat, S (n + m) = n + S m
S (m + n) = m + S n rewrite -> H'.n, m: nat
IHn: n + m = m + n
H': forall n m : nat, S (n + m) = n + S m
m + S n = m + S n by reflexivity.
Qed.

second example based on comment:

From Coq Require Import ssreflect ssrfun ssrbool.

Theorem add_comm_have' : forall n m : nat, n + m = m + n.forall n m : nat, n + m = m + n
Proof.forall n m : nat, n + m = m + n
  intros.n, m: nat
n + m = m + n induction n.m: nat
0 + m = m + 0
n, m: nat
IHn: n + m = m + n
S n + m = m + S n
  -m: nat
0 + m = m + 0 simpl.m: nat
m = m + 0
    have -> //: forall n, n + 0 = n by apply n_plus_zero_eq_n.
  -n, m: nat
IHn: n + m = m + n
S n + m = m + S n simpl.n, m: nat
IHn: n + m = m + n
S (n + m) = m + S n rewrite IHn.n, m: nat
IHn: n + m = m + n
S (m + n) = m + S n
    have -> //: forall n m: nat, S (n + m) = n + (S m)
               by apply Sn_plus_m_eq_n_plus_Sm.
Qed.

A: If you write have -> //: forall n, n + 0 = n by (apply n_plus_zero_eq_n)., you don't even need the move=> H, rewrite -> H and by reflexivity (// asks to perform trivial simplifications).