From 73c7d80adbbe8cbb77b631acb5318e1e020ad4ec Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 26 Oct 2021 15:31:24 +0200
Subject: [PATCH] Split well_founded.v out of relations.v
No changes to the contents.
---
_CoqProject | 1 +
theories/relations.v | 57 +----------------------------------------
theories/well_founded.v | 57 +++++++++++++++++++++++++++++++++++++++++
3 files changed, 59 insertions(+), 56 deletions(-)
create mode 100644 theories/well_founded.v
diff --git a/_CoqProject b/_CoqProject
index 6ea277df..78d8e4df 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -22,6 +22,7 @@ theories/countable.v
theories/orders.v
theories/natmap.v
theories/strings.v
+theories/well_founded.v
theories/relations.v
theories/sets.v
theories/listset.v
diff --git a/theories/relations.v b/theories/relations.v
index f6093bc9..34033178 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -1,7 +1,7 @@
(** This file collects definitions and theorems on abstract rewriting systems.
These are particularly useful as we define the operational semantics as a
small step semantics. *)
-From stdpp Require Export sets.
+From stdpp Require Export sets well_founded.
From stdpp Require Import options.
(** * Definitions *)
@@ -525,58 +525,3 @@ Section subrel.
Lemma rtc_subrel x y : subrel → rtc R1 x y → rtc R2 x y.
Proof. induction 2; [by apply rtc_refl|]. eapply rtc_l; eauto. Qed.
End subrel.
-
-(** * Theorems on well founded relations *)
-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; naive_solver. Qed.
-
-Notation wf := well_founded.
-
-(** 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 [wf] proofs "compute". For big enough [n], say [32], computation will
-reach implementation limits before running into the opaque [wf] 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 : wf R) : wf R :=
- Acc_intro_generator n wfR.
-
-(* 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
-computation (that is, we cannot make it opaque). We use the [Strategy]
-command to make its expanding behavior less eager. *)
-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 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 x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed.
-
-Lemma Fix_unfold_rel `{R : relation A} (wfR : wf 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.
diff --git a/theories/well_founded.v b/theories/well_founded.v
new file mode 100644
index 00000000..8eeac9e3
--- /dev/null
+++ b/theories/well_founded.v
@@ -0,0 +1,57 @@
+(** * Theorems on well founded relations *)
+From stdpp Require Import base tactics.
+From stdpp Require Import options.
+
+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; naive_solver. Qed.
+
+Notation wf := well_founded.
+
+(** 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 [wf] proofs "compute". For big enough [n], say [32], computation will
+reach implementation limits before running into the opaque [wf] 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 : wf R) : wf R :=
+ Acc_intro_generator n wfR.
+
+(* 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
+computation (that is, we cannot make it opaque). We use the [Strategy]
+command to make its expanding behavior less eager. *)
+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 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 x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed.
+
+Lemma Fix_unfold_rel `{R : relation A} (wfR : wf 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.
--
GitLab