Moving lemmas around. Map monad lemmas.

vellvm · Jun 30, 2023 · ed5949a · ed5949a
1 parent 7d441fa
commit ed5949a
Show file tree

Hide file tree

Showing 3 changed files with 150 additions and 77 deletions.
diff --git a/src/coq/Semantics/DynamicValues.v b/src/coq/Semantics/DynamicValues.v
@@ -4387,77 +4387,6 @@ Module DVALUE(A:Vellvm.Semantics.MemoryAddress.ADDRESS)(IP:Vellvm.Semantics.Memo
         end
     end.
 
-  (* TODO: Move to listutils *)
-  Lemma double_list_rect :
-    forall {X Y}
-      (P: (list X * list Y) -> Type)
-      (NilNil : P (nil, nil))
-      (NilCons : forall y ys, P (nil, ys) -> P (nil, (y :: ys)))
-      (ConsNil : forall x xs, P (xs, nil) -> P ((x :: xs), nil))
-      (ConsCons : forall x xs y ys, P (xs, ys) -> P ((x :: xs), (y :: ys))),
-    forall l, P l.
-  Proof.
-    intros X Y P NilNil NilCons ConsNil ConsCons l.
-    destruct l as [xs ys].
-    revert ys.
-    induction xs; induction ys.
-    - apply NilNil.
-    - apply NilCons.
-      apply IHys.
-    - apply ConsNil.
-      apply IHxs.
-    - apply ConsCons.
-      apply IHxs.
-  Qed.
-
-  (* TODO: move this / does this exist somewhere else? *)
-  Lemma nat_strong_rect :
-    forall (P: nat -> Type)
-      (BASE: P 0%nat)
-      (IH: forall (n : nat), (forall (m : nat), m <= n -> P m)%nat -> P (S n)),
-    forall n, P n.
-  Proof.
-    intros P BASE IH n.
-    destruct n.
-    - apply BASE.
-    - apply IH.
-      induction n; intros m LE.
-      + assert (m=0)%nat by lia; subst; auto.
-      + assert (m <= n \/ m = S n)%nat by lia.
-        pose proof NPeano.Nat.leb_spec0 m n.
-        inv H0; subst; auto.
-        pose proof NPeano.Nat.eqb_spec m (S n).
-        inv H0; subst; auto.
-        exfalso.
-        lia.
-  Qed.
-
-  (* TODO: Move to listutils *)
-  Lemma length_strong_rect:
-    forall (X : Type) (P : list X -> Type)
-      (BASE: P nil)
-      (IH: forall (n : nat) (xs: list X), (forall (xs : list X), length xs <= n -> P xs)%nat -> length xs = S n -> P xs),
-    forall l, P l.
-  Proof.
-    intros X P BASE IH.
-    assert (forall n l, length l <= n -> P l)%nat as IHLEN.
-    { induction n using nat_strong_rect; intros l LEN; auto.
-      assert (length l = 0)%nat as LEN' by lia.
-      apply length_zero_iff_nil in LEN'; subst; auto.
-
-      assert (length l <= n \/ length l = S n)%nat by lia.
-      pose proof NPeano.Nat.leb_spec0 (length l) n.
-      inv H0; subst; eauto.
-      pose proof NPeano.Nat.eqb_spec (length l) (S n).
-      inv H0; subst; eauto.
-      lia.
-    }
-
-    intros l.
-    eapply IHLEN.
-    reflexivity.
-  Qed.
-
   (* TODO: Move this *)
   Lemma vector_dtyp_dec :
     forall t,

diff --git a/src/coq/Utils/ListUtil.v b/src/coq/Utils/ListUtil.v
@@ -1352,3 +1352,81 @@ Lemma allb_forallb :
 Proof.
   induction xs; auto.
 Qed.
+
+Lemma nth_error_cons :
+  forall {X} (x : X) xs n res,
+    nth_error xs n = res ->
+    nth_error (x::xs) (S n) = res.
+Proof.
+  intros X x xs n res H.
+  cbn; auto.
+Qed.
+
+Lemma double_list_rect :
+  forall {X Y}
+    (P: (list X * list Y) -> Type)
+    (NilNil : P (nil, nil))
+    (NilCons : forall y ys, P (nil, ys) -> P (nil, (y :: ys)))
+    (ConsNil : forall x xs, P (xs, nil) -> P ((x :: xs), nil))
+    (ConsCons : forall x xs y ys, P (xs, ys) -> P ((x :: xs), (y :: ys))),
+  forall l, P l.
+Proof.
+  intros X Y P NilNil NilCons ConsNil ConsCons l.
+  destruct l as [xs ys].
+  revert ys.
+  induction xs; induction ys.
+  - apply NilNil.
+  - apply NilCons.
+    apply IHys.
+  - apply ConsNil.
+    apply IHxs.
+  - apply ConsCons.
+    apply IHxs.
+Qed.
+
+(* TODO: move this / does this exist somewhere else? *)
+Lemma nat_strong_rect :
+  forall (P: nat -> Type)
+    (BASE: P 0%nat)
+    (IH: forall (n : nat), (forall (m : nat), m <= n -> P m)%nat -> P (S n)),
+  forall n, P n.
+Proof.
+  intros P BASE IH n.
+  destruct n.
+  - apply BASE.
+  - apply IH.
+    induction n; intros m LE.
+    + assert (m=0)%nat by lia; subst; auto.
+    + assert (m <= n \/ m = S n)%nat by lia.
+      pose proof NPeano.Nat.leb_spec0 m n.
+      inv H0; subst; auto.
+      pose proof NPeano.Nat.eqb_spec m (S n).
+      inv H0; subst; auto.
+      exfalso.
+      lia.
+Qed.
+
+Lemma length_strong_rect:
+  forall (X : Type) (P : list X -> Type)
+    (BASE: P nil)
+    (IH: forall (n : nat) (xs: list X), (forall (xs : list X), length xs <= n -> P xs)%nat -> length xs = S n -> P xs),
+  forall l, P l.
+Proof.
+  intros X P BASE IH.
+  assert (forall n l, length l <= n -> P l)%nat as IHLEN.
+  { induction n using nat_strong_rect; intros l LEN; auto.
+    assert (length l = 0)%nat as LEN' by lia.
+    apply length_zero_iff_nil in LEN'; subst; auto.
+
+    assert (length l <= n \/ length l = S n)%nat by lia.
+    pose proof NPeano.Nat.leb_spec0 (length l) n.
+    inv H0; subst; eauto.
+    pose proof NPeano.Nat.eqb_spec (length l) (S n).
+    inv H0; subst; eauto.
+    lia.
+  }
+
+  intros l.
+  eapply IHLEN.
+  reflexivity.
+Qed.
diff --git a/src/coq/Utils/MapMonadExtra.v b/src/coq/Utils/MapMonadExtra.v
@@ -1,6 +1,7 @@
 From Coq Require Import
-     List
-     Morphisms.
+  String
+  List
+  Morphisms.
 
 Require Import Coq.Logic.ProofIrrelevance.
 
@@ -47,7 +48,6 @@ Section MonadContext.
   Existing Instance MRETPROPER.
   Existing Instance MRETPROPERFLIP.
 
-
 Lemma map_monad_unfold :
   forall {A B : Type} (x : A) (xs : list A)
     (f : A -> M B),
@@ -60,7 +60,6 @@ Proof.
   induction xs; cbn; auto.
 Qed.
 
-
 Lemma map_monad_length :
   forall {A B}  (xs : list A) (f : A -> M B) res,
     MReturns res (map_monad f xs) ->
@@ -86,8 +85,6 @@ Proof.
     lia.
 Qed.
 
-
-
 (* TODO: can I generalize this? *)
 Lemma map_monad_err_In :
   forall {A B} (f : A -> err B) l res x,
@@ -225,6 +222,75 @@ Proof.
       exists a'. tauto.
 Qed.
 
+Lemma map_monad_err_twin_fail :
+  forall {s1 s2 : string}
+    {X Y Z} {xs : list X} {f : X -> err Y} {g : X -> err Z}
+    (MAPM1 : map_monad f xs = inl s1)
+    (MAPM2 : map_monad g xs = inl s2)
+    (SAME_ERROR : forall x s, f x = inl s <-> g x = inl s),
+    s1 = s2.
+Proof.
+  intros s1 s2 X Y Z xs.
+  induction xs; intros f g MAPM1 MAPM2 SAME_ERROR.
+  - cbn in *.
+    inv MAPM1.
+  - cbn in *.
+    break_match_hyp_inv; break_match_hyp_inv.
+    + apply SAME_ERROR in Heqs0.
+      rewrite Heqs0 in Heqs; inv Heqs; auto.
+    + clear H0.
+      apply SAME_ERROR in Heqs.
+      rewrite Heqs0 in Heqs; inv Heqs; auto.
+    + break_match_hyp_inv.
+      * apply SAME_ERROR in Heqs1.
+        rewrite Heqs1 in Heqs; inv Heqs; auto.
+      * break_match_hyp_inv.
+        eapply IHxs; eauto.
+Qed.
+
+Lemma map_monad_err_twin_fail' :
+  forall {s1 s2 : string}
+    {X Y Z W} {xs : list X} {ys : list Y} {f : X -> err Z} {g : Y -> err W}
+    (MAPM1 : map_monad f xs = inl s1)
+    (MAPM2 : map_monad g ys = inl s2)
+    (SAME_ERROR : forall n x y s,
+        Util.Nth xs n x ->
+        Util.Nth ys n y ->
+        f x = inl s <-> g y = inl s),
+    s1 = s2.
+Proof.
+  intros s1 s2 X Y Z W xs ys.
+  remember (xs, ys) as ZIP.
+  replace xs with (fst ZIP) in * by (subst; auto).
+  replace ys with (snd ZIP) in * by (inv HeqZIP; cbn; auto).
+  clear xs ys HeqZIP.
+  induction ZIP using double_list_rect; intros f g MAPM1 MAPM2 SAME_ERROR;
+    try solve
+      [ cbn in *;
+        solve
+          [ inv MAPM1
+          | inv MAPM2
+          ]
+      ].
+
+  cbn in *.          
+  break_match_hyp_inv; break_match_hyp_inv.
+  - specialize (SAME_ERROR 0%nat x y s1 eq_refl eq_refl).
+    apply SAME_ERROR in Heqs0.
+    rewrite Heqs in Heqs0; inv Heqs0; auto.
+  - specialize (SAME_ERROR 0%nat x y s2 eq_refl eq_refl).
+    apply SAME_ERROR in Heqs.
+    rewrite Heqs in Heqs0; inv Heqs0; auto.
+  - break_match_hyp_inv.
+    + eapply (SAME_ERROR 0%nat) in Heqs1; cbn; eauto.
+      rewrite Heqs in Heqs1; inv Heqs1.
+    + break_match_hyp_inv.
+      eapply IHZIP; eauto.
+      intros n x0 y0 s H H0.
+      eapply SAME_ERROR;
+        apply nth_error_cons; eauto.
+Qed.
+
 Lemma map_monad_map :
   forall A B C
     (f : B -> M C)