From 83f1a1f84fc7c9c319e482a1d3dec7bae5813a07 Mon Sep 17 00:00:00 2001
From: Jan Tusil <jenda.tusil@gmail.com>
Date: Wed, 21 Jun 2023 18:26:46 +0200
Subject: [PATCH] automatically introduce wf premises when entering proof mode
 (#374)

* automatically introduce wf premises when entering proof mode

* ProofMode Tutorial: no need to introduce wfXY hyps
---
 examples/02_proofmode/theories/tutorial.v    |  7 +++----
 matching-logic/src/ProofMode/Basics.v        | 16 +++++++++++++++-
 matching-logic/src/ProofMode/Propositional.v |  9 ++++++---
 3 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/examples/02_proofmode/theories/tutorial.v b/examples/02_proofmode/theories/tutorial.v
index f8b0c9fa..4586f89d 100644
--- a/examples/02_proofmode/theories/tutorial.v
+++ b/examples/02_proofmode/theories/tutorial.v
@@ -217,7 +217,8 @@ Example use_rewriteBy {Σ : Signature} {syntax : Definedness_Syntax.Syntax}
     Γ ⊢ (ϕ₁ $ ϕ₄ =ml ϕ₂ $ ϕ₄ ) ---> (ϕ₁ =ml ϕ₂) ---> ((ϕ₃ $ ϕ₁ $ ϕ₄) <---> (ϕ₃ $ ϕ₂ $ ϕ₄))
 .
 Proof.
-    intros HΓ wfϕ₁ wfϕ₂ wfϕ₃ wfϕ₄.
+    intros HΓ.
+    (* Also, all the wfXY hypothesis can be introduced automatically when entering the proof mode (usually also automatically)*)
     mlIntro "H1". mlIntro "H2".
 
     (* We can rewrite using an equality from the local context. *)
@@ -261,7 +262,7 @@ Example use_rewriteBy {Σ : Signature} {syntax : Definedness_Syntax.Syntax}
     Γ ⊢ (ϕ₁ $ ϕ₄ =ml ϕ₂ $ ϕ₄ ) ---> (ϕ₁ =ml ϕ₂) ---> ((ϕ₃ $ ϕ₁ $ ϕ₄) <---> (ϕ₃ $ ϕ₂ $ ϕ₄))
 .
 Proof.
-    intros HΓ Hmf wfϕ₁ wfϕ₂ wfϕ₃ wfϕ₄.
+    intros HΓ Hmf.
     mlIntro "H1". mlIntro "H2".
 
     (* We can rewrite using an equality from the local context. *)
@@ -299,7 +300,6 @@ Example use_mlApply {Σ : Signature} (Γ : Theory) (a b c : Pattern) :
     well_formed c = true ->
     Γ ⊢ (a ---> b $ c) ---> (b $ c ---> c) ---> (a ---> c).
 Proof.
-    intros wfa wfb wfc.
     mlIntro "H1". mlIntro "H2". mlIntro "H3".
     (* strenghtens the concusion using H2 *)
     mlApply "H2".
@@ -322,7 +322,6 @@ Example use_mlApplyMeta {Σ : Signature} (Γ : Theory) (a b c d : Pattern) :
     well_formed d = true ->
     Γ ⊢ a ---> ((ex, c) $ d) ---> b ---> (ex, (c $ d)).
 Proof.
-    intros wfa wfb wfc wfd.
     mlIntro "H1". mlIntro "H2". mlIntro "H3".
 
     Check Prop_ex_left.
diff --git a/matching-logic/src/ProofMode/Basics.v b/matching-logic/src/ProofMode/Basics.v
index 12f2c987..cbd5d3f8 100644
--- a/matching-logic/src/ProofMode/Basics.v
+++ b/matching-logic/src/ProofMode/Basics.v
@@ -319,8 +319,22 @@ lazymatch goal with
   end
 end.
 
+Ltac _introAllWf :=
+  unfold is_true;
+  repeat (
+    lazymatch goal with
+    | [ |- well_formed _ = true -> _ ] =>
+      let H := fresh "Hwf" in
+      intros H
+    | [ |- Pattern.wf _ = true -> _ ] =>
+      let H := fresh "Hwfl" in
+      intros H
+    end
+  )
+.
+
 Ltac _enterProofMode :=
-  toMLGoal;[wf_auto2|]
+  _introAllWf;toMLGoal;[wf_auto2|]
 .
 
 Ltac _ensureProofMode :=
diff --git a/matching-logic/src/ProofMode/Propositional.v b/matching-logic/src/ProofMode/Propositional.v
index e6801953..947637ef 100644
--- a/matching-logic/src/ProofMode/Propositional.v
+++ b/matching-logic/src/ProofMode/Propositional.v
@@ -104,9 +104,12 @@ Local Example ex_mlExact {Σ : Signature} Γ a b c:
   well_formed c = true ->
   Γ ⊢i a ---> b ---> c ---> b using BasicReasoning.
 Proof.
-  intros wfa wfb wfc.
-  toMLGoal.
-  { wf_auto2. }
+  (* The following are not necessary *)
+  (*
+    intros wfa wfb wfc.
+    toMLGoal.
+    { wf_auto2. }
+  *)
   mlIntro "H1". mlIntro "H2". mlIntro "H3". (* TODO: mlIntros "H1" "H2" "H3".*)
   mlExact "H2".
 Defined.