Merge branch 'robbert/wn' into 'master'

Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.

See merge request iris/stdpp!140

CHANGELOG.md

@@ -59,6 +59,7 @@ Noteworthy additions and changes:
   + Add `NoDup_seqZ` and `Forall_seqZ`
 - Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
   `singletonM` and to avoid overlap with `sets.singleton_proper`.
+- Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):

theories/relations.v

@@ -57,7 +57,9 @@ End definitions.
 (** The reflexive transitive symmetric closure. *)
 Definition rtsc {A} (R : relation A) := rtc (sc R).
 
-(** Strongly normalizing elements. *)
+(** Weakly and strongly normalizing elements. *)
+Definition wn {A} (R : relation A) (x : A) := ∃ y, rtc R x y ∧ nf R y.
+
 Notation sn R := (Acc (flip R)).
 
 (** The various kinds of "confluence" properties. Any relation that has the
@@ -271,8 +273,23 @@ Section properties.
 
   Hint Constructors rtc nsteps bsteps tc : core.
 
-  Lemma acc_not_ex_loop x : Acc (flip R) x → ¬ex_loop R x.
-  Proof. unfold not. induction 1; destruct 1; eauto. Qed.
+  Lemma nf_wn x : nf R x → wn R x.
+  Proof. intros. exists x; eauto. Qed.
+  Lemma wn_step x y : wn R y → R x y → wn R x.
+  Proof. intros (z & ? & ?) ?. exists z; eauto. Qed.
+  Lemma wn_step_rtc x y : wn R y → rtc R x y → wn R x.
+  Proof. induction 2; eauto using wn_step. Qed.
+
+  (** The following theorem requires that [red R] is decidable. The intuition
+  for this requirement is that [wn R] is a very "positive" statement as it
+  points out a particular trace. In contrast, [sn R] just says "this also holds
+  for all successors", there is no "data"/"trace" there. *)
+  Lemma sn_wn `{!∀ y, Decision (red R y)} x : sn R x → wn R x.
+  Proof.
+    induction 1 as [x _ IH]. destruct (decide (red R x)) as [[x' ?]|?].
+    - destruct (IH x') as (y&?&?); eauto using wn_step.
+    - by apply nf_wf.
+  Qed.
 
   Lemma all_loop_red x : all_loop R x → red R x.
   Proof. destruct 1; auto. Qed.
@@ -288,6 +305,11 @@ Section properties.
     cofix FIX. constructor; eauto using rtc_r.
   Qed.
 
+  Lemma wn_not_all_loop x : wn R x → ¬all_loop R x.
+  Proof. intros (z&?&?). rewrite all_loop_alt. eauto. Qed.
+  Lemma sn_not_ex_loop x : sn R x → ¬ex_loop R x.
+  Proof. unfold not. induction 1; destruct 1; eauto. Qed.
+
   (** An alternative definition of confluence; also known as the Church-Rosser
   property. *)
   Lemma confluent_alt :