mapi proper, -1 admit

rems-project · Nov 8, 2023 · 5ca9aa8 · 5ca9aa8
1 parent 8e624c4
commit 5ca9aa8
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 26 deletions.
diff --git a/coq/Common/Utils.v b/coq/Common/Utils.v
@@ -75,19 +75,10 @@ Definition bool_list_cmp (a b: list bool) : bool :=
 Definition mem {A:Type} `{forall (x y:A), Decidable (x = y)} (a:A): (list A) -> bool
   := List.existsb (fun e => decide (e = a)).
 
-Definition mapi {A B: Type} (f: nat -> A -> B) (l:list A) : list B :=
-  let fix map_ n (l:list A) :=
-    match l with
-    | [] => []
-    | a :: t => (f n a) :: (map_ (S n) t)
-    end
-  in map_ O l.
-
-(* alternative definition of [mapi] *)
-Fixpoint mapi' {A B: Type} (f: nat -> A -> B) (l:list A) : list B :=
+Fixpoint mapi {A B: Type} (f: nat -> A -> B) (l:list A) : list B :=
   match l with
   | [] => []
-  | x :: xs => (f O x) :: (mapi' (fun n v => f (S n) v) xs)
+  | x :: xs => (f O x) :: (mapi (fun n v => f (S n) v) xs)
   end.
 
 (* c.f.

diff --git a/coq/Proofs/ProofsAux.v b/coq/Proofs/ProofsAux.v
@@ -73,16 +73,31 @@ Section ListAux.
         reflexivity.
   Qed.
 
-  (* Now we can prove that mapi is Proper with respect to eqlistA. *)
-  #[global] Lemma list_mapi_Proper
+
+  Lemma mapi_cons  {A B : Type} x l {f: nat -> A -> B}:
+    mapi f (x :: l) = f 0 x :: mapi (compose f S) l.
+  Proof. auto. Qed.
+
+  #[global] Instance list_mapi_Proper
     {A B : Type}
-    (f : nat -> A -> B)
     (pA: relation A)
     (pB: relation B)
-    {Hf: Proper (eq ==> pA ==> pB) f}:
-    Proper (eqlistA pA ==> eqlistA pB) (mapi f).
+    :
+    Proper (pointwise_relation _ (pA ==> pB) ==> (eqlistA pA ==> eqlistA pB))
+      mapi.
   Proof.
-  Admitted.
+    intros f f' Hf l l' Hl. revert f f' Hf.
+    induction Hl as [|x1 x2 l1 l2 ?? IH]; intros f f' Hf.
+    - constructor.
+    -
+      cbn.
+      constructor.
+      +
+        apply Hf, H.
+      +
+        apply IH. intros i y y' ?.
+        apply Hf, H0.
+  Qed.
 
 End ListAux.
 
@@ -250,7 +265,7 @@ Section ZMapAux.
 
   #[global] Instance zmap_range_init_Proper:
     forall [elt : Type], Proper (eq ==> eq ==> eq ==> eq ==> ZMap.Equal ==> ZMap.Equal)
-                      (zmap_range_init (T:=elt)).
+                           (zmap_range_init (T:=elt)).
   Proof.
     intros elt a1 a0 EA n0 n EN s0 s ES v0 v EV m0 m1 EM k.
     subst.

diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -1456,8 +1456,8 @@ Module RevocationProofs.
               rewrite H3.
               reflexivity.
             + apply list_mapi_Proper with (pA:=AbsByte_eq) (pB:=Z_AbsByte_eq).
-              * intros l1 l2 LE a1 a2 AE.
-                subst.
+              *
+                intros n a1 a2 AE.
                 constructor.
                 reflexivity.
                 assumption.
@@ -1474,8 +1474,8 @@ Module RevocationProofs.
               rewrite H3.
               reflexivity.
             + apply list_mapi_Proper with (pA:=AbsByte_eq) (pB:=Z_AbsByte_eq).
-              * intros l1 l2 LE a1 a2 AE.
-                subst.
+              *
+                intros n a1 a2 AE.
                 constructor.
                 reflexivity.
                 assumption.
@@ -1513,8 +1513,7 @@ Module RevocationProofs.
               rewrite H5.
               reflexivity.
             + apply list_mapi_Proper with (pA:=AbsByte_eq) (pB:=Z_AbsByte_eq).
-              * intros l1 l2 LE a1 a2 AE.
-                subst.
+              * intros n a1 a2 AE.
                 constructor.
                 reflexivity.
                 assumption.
@@ -1553,8 +1552,7 @@ Module RevocationProofs.
               rewrite H5.
               reflexivity.
             + apply list_mapi_Proper with (pA:=AbsByte_eq) (pB:=Z_AbsByte_eq).
-              * intros l1 l2 LE a1 a2 AE.
-                subst.
+              * intros n a1 a2 AE.
                 constructor.
                 reflexivity.
                 assumption.