Another try at fix_sub_eq_ext

progs/verif_io.v

@@ -130,6 +130,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -138,7 +156,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -230,7 +248,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.
 

progs/verif_io_mem.v

@@ -116,6 +116,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.*)
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -124,7 +142,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -226,7 +244,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.
 

progs64/verif_io.v

@@ -130,6 +130,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -138,7 +156,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -230,7 +248,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.
 

progs64/verif_io_mem.v

@@ -116,6 +116,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.*)
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -124,7 +142,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -226,7 +244,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.