Commit c92654ed by Robbert Krebbers

### Define `wf_guard` in terms of Coq stdlib's `Acc_intro_generator`.

parent b9ef84b4
 ... @@ -194,33 +194,8 @@ End subrel. ... @@ -194,33 +194,8 @@ End subrel. (** * Theorems on well founded relations *) (** * Theorems on well founded relations *) Notation wf := well_founded. Notation wf := well_founded. Definition wf_guard `{R : relation A} (n : nat) (wfR : wf R) : wf R := Section wf. Acc_intro_generator n wfR. Context `{R : relation A}. Lemma Acc_def x : Acc R x ↔ (∀ y : A, R y x → Acc R y). Proof. split. by destruct 1. by constructor. Qed. (** A trick by Thomas Braibant to compute with well-founded recursions: it lazily adds [2^n] [Acc_intro] constructors in front of a well foundedness proof, so that the actual proof is never reached in practise. *) Fixpoint wf_guard (n : nat) (wfR : wf R) : wf R := match n with | 0 => wfR | S n => λ x, Acc_intro x (λ y _, wf_guard n (wf_guard n wfR) y) end. Lemma wf_projected `(R2 : relation B) (f : A → B) : (∀ x y, R x y → R2 (f x) (f y)) → wf R2 → wf R. Proof. intros Hf Hwf. cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R x). { intros aux x. apply (aux (f x)); auto. } induction 1 as [y _ IH]. intros x ?. subst. constructor. intros. apply (IH (f y)); auto. Qed. End wf. (* Generally we do not want [wf_guard] to be expanded (neither by tactics, (* Generally we do not want [wf_guard] to be expanded (neither by tactics, nor by conversion tests in the kernel), but in some cases we do need it for nor by conversion tests in the kernel), but in some cases we do need it for ... @@ -228,6 +203,17 @@ computation (that is, we cannot make it opaque). We use the [Strategy] ... @@ -228,6 +203,17 @@ computation (that is, we cannot make it opaque). We use the [Strategy] command to make its expanding behavior less eager. *) command to make its expanding behavior less eager. *) Strategy 100 [wf_guard]. 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)) → wf R2 → wf 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. apply (IH (f y)); auto. Qed. Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x)) 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) (F : ∀ x, (∀ y, R y x → B y) → B x) (HF : ∀ (x : A) (f g : ∀ y, R y x → B y), (HF : ∀ (x : A) (f g : ∀ y, R y x → B y), ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!