Merge branch 'choose_proper' into 'master'

countable.v: prove choose_proper

See merge request iris/stdpp!327

CHANGELOG.md

@@ -170,6 +170,13 @@ API-breaking change is listed.
   slightly weaker in case the left-hand side and right-hand side of the relation
   call a function with arguments that are convertible but not syntactically
   equal.
+- Add lemma `choose_proper` showing that `choose P` respects predicate
+  equivalence. (by Paolo G. Giarrusso, BedRock Systems)
+- Extract module `well_founded` from `relations`, and re-export it for
+  compatibility. This contains `wf`, `Acc_impl`, `wf_guard`,
+  `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`.
+- Add induction principle `well_founded.Acc_dep_ind`, a dependent
+  version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

_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

theories/countable.v

 From Coq.QArith Require Import QArith_base Qcanon.
 From stdpp Require Export list numbers list_numbers fin.
+From stdpp Require Import well_founded.
 From stdpp Require Import options.
 Local Open Scope positive.
 
@@ -89,6 +90,25 @@ Section choice.
   Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
 End choice.
 
+Section choice_proper.
+  Context `{Countable A}.
+  Context (P1 P2 : A → Prop) `{∀ x, Decision (P1 x)} `{∀ x, Decision (P2 x)}.
+  Context (Heq : ∀ x, P1 x ↔ P2 x).
+
+  Lemma choose_go_proper {i} (acc1 acc2 : Acc (choose_step _) i) :
+    choose_go P1 acc1 = choose_go P2 acc2.
+  Proof using Heq.
+    induction acc1 as [i a1 IH] using Acc_dep_ind;
+      destruct acc2 as [acc2]; simpl.
+    destruct (Some_dec _) as [[x Hx]|]; [|done].
+    do 2 case_decide; done || exfalso; naive_solver.
+  Qed.
+
+  Lemma choose_proper p1 p2 :
+    choose P1 p1 = choose P2 p2.
+  Proof using Heq. apply choose_go_proper. Qed.
+End choice_proper.
+
 Lemma surj_cancel `{Countable A} `{EqDecision B}
   (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }.
 Proof.

theories/relations.v

 (** 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 Coq Require Import Wf_nat.
-From stdpp Require Export sets.
+From stdpp Require Export sets well_founded.
 From stdpp Require Import options.
 
 (** * Definitions *)
@@ -526,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.

theories/well_founded.v

+(** * Theorems on well founded relations *)
+From stdpp Require Import base.
+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; auto. 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.
+
+(**
+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.