Library stdpp.well_founded
Generate an induction principle for Acc for reasoning about recursion on
Acc, such as countable.choose_proper.
We need an induction principle to prove predicates of Acc values, with
conclusion ∀ (x : A) (a : Acc R x), P x a. Instead, Acc_ind has conclusion
∀ x : A, Acc R x → P x, as if it were generated by
Scheme Acc_rect := Minimality for Acc Sort Prop.
Scheme Acc_dep_ind := Induction for Acc Sort Prop.
Lemma Acc_impl {A} (R1 R2 : relation A) x :
Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x.
Proof. induction 1; constructor; auto. Qed.
Lemma Acc_impl {A} (R1 R2 : relation A) x :
Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x.
Proof. induction 1; constructor; auto. Qed.
The function wf_guard n wfR adds 2 ^ n - 1 times an Acc_intro
constructor ahead of the wfR proof. This definition can be used to make
opaque well_founded proofs "compute". For big enough n, say 32, computation will
reach implementation limits before running into the opaque well_founded proof.
This trick is originally due to Georges Gonthier, see
https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html
Definition wf_guard `{R : relation A} (n : nat)
(wfR : well_founded R) : well_founded R :=
Acc_intro_generator n wfR.
Strategy 100 [wf_guard].
Lemma wf_projected `{R1 : relation A} `(R2 : relation B) (f : A → B) :
(∀ x y, R1 x y → R2 (f x) (f y)) →
well_founded R2 → well_founded R1.
Proof.
intros Hf Hwf.
cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x).
{ intros aux x. apply (aux (f x)); auto. }
induction 1 as [y _ IH]. intros x ?. subst.
constructor. intros y ?. apply (IH (f y)); auto.
Qed.
Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x))
(F : ∀ x, (∀ y, R y x → B y) → B x)
(HF : ∀ (x : A) (f g : ∀ y, R y x → B y),
(∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
(x : A) (acc1 acc2 : Acc R x) :
E _ (Fix_F B F acc1) (Fix_F B F acc2).
Proof.
revert acc2. induction acc1 using Acc_dep_ind; intros []; simpl; auto.
Qed.
Lemma Fix_unfold_rel `{R : relation A} (wfR : well_founded R)
(B : A → Type) (E : ∀ x, relation (B x))
(F: ∀ x, (∀ y, R y x → B y) → B x)
(HF: ∀ (x: A) (f g: ∀ y, R y x → B y),
(∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
(x: A) :
E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)).
Proof.
unfold Fix.
destruct (wfR x); simpl.
apply HF; intros.
apply Fix_F_proper; auto.
Qed.
(wfR : well_founded R) : well_founded R :=
Acc_intro_generator n wfR.
Strategy 100 [wf_guard].
Lemma wf_projected `{R1 : relation A} `(R2 : relation B) (f : A → B) :
(∀ x y, R1 x y → R2 (f x) (f y)) →
well_founded R2 → well_founded R1.
Proof.
intros Hf Hwf.
cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x).
{ intros aux x. apply (aux (f x)); auto. }
induction 1 as [y _ IH]. intros x ?. subst.
constructor. intros y ?. apply (IH (f y)); auto.
Qed.
Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x))
(F : ∀ x, (∀ y, R y x → B y) → B x)
(HF : ∀ (x : A) (f g : ∀ y, R y x → B y),
(∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
(x : A) (acc1 acc2 : Acc R x) :
E _ (Fix_F B F acc1) (Fix_F B F acc2).
Proof.
revert acc2. induction acc1 using Acc_dep_ind; intros []; simpl; auto.
Qed.
Lemma Fix_unfold_rel `{R : relation A} (wfR : well_founded R)
(B : A → Type) (E : ∀ x, relation (B x))
(F: ∀ x, (∀ y, R y x → B y) → B x)
(HF: ∀ (x: A) (f g: ∀ y, R y x → B y),
(∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
(x: A) :
E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)).
Proof.
unfold Fix.
destruct (wfR x); simpl.
apply HF; intros.
apply Fix_F_proper; auto.
Qed.