| Authors: Bruno Barras, Cristina Cornes |
Require Import Eqdep.
Require Import Relation_Operators.
Require Import Transitive_Closure.
| From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 |
Section WfLexicographic_Product.
Variable A : Set.
Variable B : A -> Set.
Variable leA : A -> A -> Prop.
Variable leB : forall x:A, B x -> B x -> Prop.
Notation LexProd := (lexprod A B leA leB).
Hint Resolve t_step Acc_clos_trans wf_clos_trans.
Lemma acc_A_B_lexprod :
forall x:A,
Acc leA x ->
(forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) ->
forall y:B x, Acc (leB x) y -> Acc LexProd (existS B x y).
Proof.
induction 1 as [x _ IHAcc]; intros H2 y.
induction 1 as [x0 H IHAcc0]; intros.
apply Acc_intro.
destruct y as [x2 y1]; intro H6.
simple inversion H6; intro.
cut (leA x2 x); intros.
apply IHAcc; auto with sets.
intros.
apply H2.
apply t_trans with x2; auto with sets.
red in H2.
apply H2.
auto with sets.
injection H1.
destruct 2.
injection H3.
destruct 2; auto with sets.
rewrite <- H1.
injection H3; intros _ Hx1.
subst x1.
apply IHAcc0.
elim inj_pair2 with A B x y' x0; assumption.
Qed.
Theorem wf_lexprod :
well_founded leA ->
(forall x:A, well_founded (leB x)) -> well_founded LexProd.
Proof.
intros wfA wfB; unfold well_founded in |- *.
destruct a.
apply acc_A_B_lexprod; auto with sets; intros.
red in wfB.
auto with sets.
Qed.
End WfLexicographic_Product.
Section Wf_Symmetric_Product.
Variable A : Set.
Variable B : Set.
Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
Notation Symprod := (symprod A B leA leB).
Lemma Acc_symprod :
forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y).
Proof.
induction 1 as [x _ IHAcc]; intros y H2.
induction H2 as [x1 H3 IHAcc1].
apply Acc_intro; intros y H5.
inversion_clear H5; auto with sets.
apply IHAcc; auto.
apply Acc_intro; trivial.
Qed.
Lemma wf_symprod :
well_founded leA -> well_founded leB -> well_founded Symprod.
Proof.
red in |- *.
destruct a.
apply Acc_symprod; auto with sets.
Qed.
End Wf_Symmetric_Product.
Section Swap.
Variable A : Set.
Variable R : A -> A -> Prop.
Notation SwapProd := (swapprod A R).
Lemma swap_Acc : forall x y:A, Acc SwapProd (x, y) -> Acc SwapProd (y, x).
Proof.
intros.
inversion_clear H.
apply Acc_intro.
destruct y0; intros.
inversion_clear H; inversion_clear H1; apply H0.
apply sp_swap.
apply right_sym; auto with sets.
apply sp_swap.
apply left_sym; auto with sets.
apply sp_noswap.
apply right_sym; auto with sets.
apply sp_noswap.
apply left_sym; auto with sets.
Qed.
Lemma Acc_swapprod :
forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y).
Proof.
induction 1 as [x0 _ IHAcc0]; intros H2.
cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)).
clear IHAcc0.
induction H2 as [x1 _ IHAcc1]; intros H4.
cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).
clear IHAcc1.
intro.
apply Acc_intro.
destruct y; intro H5.
inversion_clear H5.
inversion_clear H0; auto with sets.
apply swap_Acc.
inversion_clear H0; auto with sets.
intros.
apply IHAcc1; auto with sets; intros.
apply Acc_inv with (y0, x1); auto with sets.
apply sp_noswap.
apply right_sym; auto with sets.
auto with sets.
Qed.
Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
Proof.
red in |- *.
destruct a; intros.
apply Acc_swapprod; auto with sets.
Qed.
End Swap.