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
harp-project · Jun 21, 2023 · 83f1a1f · 83f1a1f
1 parent 37a0046
commit 83f1a1f
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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.