diff options
Diffstat (limited to 'theories/Program/Wf.v')
| -rw-r--r-- | theories/Program/Wf.v | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 2a7a5e17..d89919b0 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,6 +11,7 @@ Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. +Require Import FunctionalExtensionality. Local Open Scope program_scope. @@ -32,14 +33,13 @@ Section Well_founded. (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *) (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *) - Hypothesis - F_ext : + Hypothesis F_ext : forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), - (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. + (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g. Lemma Fix_F_eq : forall (x:A) (r:Acc R x), - F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. + F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. Proof. destruct r using Acc_inv_dep; auto. Qed. @@ -50,7 +50,7 @@ Section Well_founded. rewrite (proof_irrelevance (Acc R x) r s) ; auto. Qed. - Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)). + Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)). Proof. intro x; unfold Fix_sub. rewrite <- (Fix_F_eq ). @@ -62,7 +62,8 @@ Section Well_founded. forall x : A, Fix_sub x = let f_sub := F_sub in - f_sub x (fun (y : A | R y x) => Fix_sub (`y)). + f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)). + Proof. exact Fix_eq. Qed. @@ -153,7 +154,7 @@ Section Fix_rects. Hypothesis equiv_lowers: forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)), - (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) -> + (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist (*FIXME shouldn't be needed *) (fun y => R y x0) x p')) -> f g = f h. (* From equiv_lowers, it follows that @@ -221,8 +222,6 @@ Ltac fold_sub f := Module WfExtensionality. - Require Import FunctionalExtensionality. - (** The two following lemmas allow to unfold a well-founded fixpoint definition without restriction using the functional extensionality axiom. *) @@ -231,10 +230,10 @@ Module WfExtensionality. Program Lemma fix_sub_eq_ext : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R) (P : A -> Type) - (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), + (F_sub : forall x : A, (forall y:{y : A | R y x}, P (` y)) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = - F_sub x (fun (y : A | R y x) => Fix_sub A R Rwf P F_sub y). + F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)). Proof. intros ; apply Fix_eq ; auto. intros. |