Fix a bug in pclearbot using pclearbotH

Author: gilhur

metasrc/pacotac.py

@@ -80,12 +80,37 @@
 (** ** [pclearbot] simplifies all hypotheses of the form [upaco{n} gf bot{n}] to [paco{n} gf bot{n}].
 *)
 
+Definition pclearbot_orL (P Q: Prop) := P.
+Definition pclearbot_orR (P Q: Prop) := Q.
+
+Ltac pclearbotH H :=
+  generalize _paco_mark_cons;
+  let NH := fresh H in
+  revert_until H;
+  repeat red in H;
+  match goal with [Hcrr: context f [or] |- _] =>
+    match Hcrr with H =>
+    first[(
+      let P := context f [pclearbot_orL] in
+      assert (NH: P) by (repeat intro; edestruct H ; [eassumption|repeat (match goal with [X: _ \/ _ |- _] => destruct X end); contradiction]);
+      clear H; rename NH into H; unfold pclearbot_orL in H
+    ) | (
+      let P := context f [pclearbot_orR] in
+      assert (NH: P) by (repeat intro; edestruct H ; [repeat (match goal with [X: _ \/ _ |- _] => destruct X end); contradiction|eassumption]);
+      clear H; rename NH into H; unfold pclearbot_orR in H
+    )]
+    end
+  end;
+  intros; paco_revert_hyp _paco_mark.
+
 Ltac pclearbot :=
-  repeat match goal with
+  repeat (
+    match goal with
 """,end="")
 for i in range(n+1):
-    print ("  | [H: context [bot"+str(i)+"] |- _] => destruct H as [H|H]; [|inversion H]")
-print ("""  end.
+    print ("    | [H: context [bot"+str(i)+"] |- _] => pclearbotH H")
+print ("""    end).
+
 
 (** ** [pdestruct H] and [pinversion H]
 *)

src/examples.v

@@ -310,3 +310,25 @@ Lemma seq_trans : forall d1 d2 d3
 Proof.
   eauto using gseq_trans, seq_implies_gseq, gseq_implies_seq.
 Qed.
+
+(**
+  Tests for [pclearbot]
+ **)
+
+Lemma plcearbot_test1 x y
+  (H: upaco2 seq_step bot2 x y)
+  :
+  True.
+Proof.
+  pclearbot.
+  eauto.
+Qed.
+
+Lemma plcearbot_test2
+  (H: forall x y, upaco2 seq_step bot2 x y)
+  :
+  True.
+Proof.
+  pclearbot.
+  eauto.
+Qed.

src/pacotac.v

@@ -69,24 +69,49 @@ Tactic Notation "pcofix" ident(CIH) := pcofix CIH with r.
 (** ** [pclearbot] simplifies all hypotheses of the form [upaco{n} gf bot{n}] to [paco{n} gf bot{n}].
 *)
 
+Definition pclearbot_orL (P Q: Prop) := P.
+Definition pclearbot_orR (P Q: Prop) := Q.
+
+Ltac pclearbotH H :=
+  generalize _paco_mark_cons;
+  let NH := fresh H in
+  revert_until H;
+  repeat red in H;
+  match goal with [Hcrr: context f [or] |- _] =>
+    match Hcrr with H =>
+    first[(
+      let P := context f [pclearbot_orL] in
+      assert (NH: P) by (repeat intro; edestruct H ; [eassumption|repeat (match goal with [X: _ \/ _ |- _] => destruct X end); contradiction]);
+      clear H; rename NH into H; unfold pclearbot_orL in H
+    ) | (
+      let P := context f [pclearbot_orR] in
+      assert (NH: P) by (repeat intro; edestruct H ; [repeat (match goal with [X: _ \/ _ |- _] => destruct X end); contradiction|eassumption]);
+      clear H; rename NH into H; unfold pclearbot_orR in H
+    )]
+    end
+  end;
+  intros; paco_revert_hyp _paco_mark.
+
 Ltac pclearbot :=
-  repeat match goal with
-  | [H: context [bot0] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot1] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot2] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot3] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot4] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot5] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot6] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot7] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot8] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot9] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot10] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot11] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot12] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot13] |- _] => destruct H as [H|H]; [|inversion H]
-  | [H: context [bot14] |- _] => destruct H as [H|H]; [|inversion H]
-  end.
+  repeat (
+    match goal with
+    | [H: context [bot0] |- _] => pclearbotH H
+    | [H: context [bot1] |- _] => pclearbotH H
+    | [H: context [bot2] |- _] => pclearbotH H
+    | [H: context [bot3] |- _] => pclearbotH H
+    | [H: context [bot4] |- _] => pclearbotH H
+    | [H: context [bot5] |- _] => pclearbotH H
+    | [H: context [bot6] |- _] => pclearbotH H
+    | [H: context [bot7] |- _] => pclearbotH H
+    | [H: context [bot8] |- _] => pclearbotH H
+    | [H: context [bot9] |- _] => pclearbotH H
+    | [H: context [bot10] |- _] => pclearbotH H
+    | [H: context [bot11] |- _] => pclearbotH H
+    | [H: context [bot12] |- _] => pclearbotH H
+    | [H: context [bot13] |- _] => pclearbotH H
+    | [H: context [bot14] |- _] => pclearbotH H
+    end).
+
 
 (** ** [pdestruct H] and [pinversion H]
 *)