diff options
Diffstat (limited to 'theories/Program/Wf.v')
| -rw-r--r-- | theories/Program/Wf.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d1be8812e9..69873d0321 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -43,7 +43,7 @@ Section Well_founded. forall (x:A) (r:Acc R x), 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. + intros x r; destruct r using Acc_inv_dep; auto. Qed. Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s. @@ -95,12 +95,12 @@ Section Measure_well_founded. Proof with auto. unfold well_founded. cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). - + intros. + + intros H a. apply (H (m a))... + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). - intros. + intros ? H ? H0. apply Acc_intro. - intros. + intros y H1. unfold MR in H1. rewrite H0 in H1. apply (H (m y))... @@ -174,7 +174,7 @@ Section Fix_rects. revert a'. pattern x, (Fix_F_sub A R P f x a). apply Fix_F_sub_rect. - intros. + intros ? H **. rewrite F_unfold. apply equiv_lowers. intros. @@ -197,11 +197,11 @@ Section Fix_rects. : forall x, Q _ (Fix_sub A R Rwf P f x). Proof with auto. unfold Fix_sub. - intros. + intros x. apply Fix_F_sub_rect. - intros. - assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))... - set (inv x0 X0 a). clearbody q. + intros x0 H a. + assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))) as X0... + set (q := inv x0 X0 a). clearbody q. rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... @@ -242,9 +242,9 @@ Module WfExtensionality. 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 (` y)). Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). + 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. |