Lvc.Infra.Relations
Require Import Arith Coq.Lists.List Setoid Coq.Lists.SetoidList Util.
Require Export Infra.Option EqDec AutoIndTac Tactics.
Set Implicit Arguments.
Require Export Infra.Option EqDec AutoIndTac Tactics.
Set Implicit Arguments.
Relations
The development in this file are based on the material of the Semantics lecture 2011 at Saarland University.
Section Unary.
Variable R : rel.
Definition reflexive :=
∀ x, R x x.
Definition symmetric :=
∀ x y, R x y → R y x.
Definition transitive :=
∀ x y z, R x y → R y z → R x z.
Definition functional :=
∀ x y z, R x y → R x z → y=z.
Definition reducible (x : X) :=
∃ y, R x y.
Definition normal (x : X) :=
¬ reducible x.
Definition total :=
∀ x, reducible x.
Hint Unfold symmetric transitive functional reducible normal total.
Variable R : rel.
Definition reflexive :=
∀ x, R x x.
Definition symmetric :=
∀ x y, R x y → R y x.
Definition transitive :=
∀ x y z, R x y → R y z → R x z.
Definition functional :=
∀ x y z, R x y → R x z → y=z.
Definition reducible (x : X) :=
∃ y, R x y.
Definition normal (x : X) :=
¬ reducible x.
Definition total :=
∀ x, reducible x.
Hint Unfold symmetric transitive functional reducible normal total.
Inductive star : rel :=
| star_refl : ∀ x, star x x
| S_star : ∀ y x z, R x y → star y z → star x z.
CoInductive diverges : X → Prop :=
| DivergesI x y : R x y → diverges y → diverges x.
Lemma star_trans (x y z:X)
: star x y → star y z → star x z.
Lemma star_right (x y z:X)
: star x y → R y z → star x z.
Inductive starn : nat → X → X → Prop :=
| starn_refl : ∀ a, starn 0 a a
| S_starn : ∀ x y z n, R x y → starn n y z → starn (S n) x z.
Lemma starn_one
: ∀ x y, R x y → starn (S 0) x y.
Lemma starn_trans n m :
∀ x y, starn n x y → ∀ z, starn m y z → starn (n+m) x z.
Lemma star0_is_eq a b
: starn 0 a b → a = b.
Lemma starn_iff_star a b
: star a b ↔ ∃ n, starn n a b.
Inductive plus : rel :=
| plusO x y : R x y → plus x y
| plusS x y z : R x y → plus y z → plus x z.
Lemma plus_trans x y z :
plus x y → plus y z → plus x z.
Lemma star_plus x y z:
R x y → star y z → plus x z.
Lemma plus_right x y z :
plus x y → R y z → plus x z.
Lemma plus_star x y :
plus x y → star x y.
Lemma star_plus_plus : ∀ x y z, star x y → plus y z → plus x z.
Lemma plus_destr x z
: plus x z → ∃ y, R x y ∧ star y z.
Lemma star_destr : ∀ x z, star x z → (x = z) ∨ plus x z.
| plusO x y : R x y → plus x y
| plusS x y z : R x y → plus y z → plus x z.
Lemma plus_trans x y z :
plus x y → plus y z → plus x z.
Lemma star_plus x y z:
R x y → star y z → plus x z.
Lemma plus_right x y z :
plus x y → R y z → plus x z.
Lemma plus_star x y :
plus x y → star x y.
Lemma star_plus_plus : ∀ x y z, star x y → plus y z → plus x z.
Lemma plus_destr x z
: plus x z → ∃ y, R x y ∧ star y z.
Lemma star_destr : ∀ x z, star x z → (x = z) ∨ plus x z.
Inductive terminates : X → Prop :=
| terminatesI x : (∀ y, R x y → terminates y) → terminates x.
Definition terminating : Prop :=
∀ x, terminates x.
Definition normalizes´ (x:X) : Prop :=
∃ y, inhabited (star x y) ∧ normal y.
Inductive normalizes : X → Prop :=
| normalizesI1 x : normal x → normalizes x
| normalizesI2 x y : R x y → normalizes y → normalizes x.
Lemma normalizes_normalizes´_agree (x:X) :
normalizes´ x ↔ normalizes x.
Definition normalizing : Prop :=
∀ x, normalizes x.
Lemma functional_normalizes_terminates x
: functional → normalizes x → terminates x.
End Unary.
Lemma star_starplus (R : rel) (x y : X)
: star R x y → star (plus R) x y.
Lemma star_idem_1 R x y
: star (star R) x y → star R x y.
Lemma star_idem_2 R x y
: star R x y → star (star R) x y.
Lemma div_plus´ : ∀ (R : rel) (x y : X), star R x y → diverges (plus R) y → diverges R x.
Lemma div_ext_star : ∀ (R : rel) (x y : X), star R x y → diverges (plus R) y → diverges (plus R) x.
Lemma div_plus : ∀ (R : rel) (x : X), diverges (plus R) x → diverges R x.
Lemma div_ext_star_2 (R: rel) x y
: functional R → diverges R x → star R x y → diverges R y.
Lemma div_ext_plus (R: rel) x y
: functional R → diverges R x → plus R x y → diverges R y.
Lemma normal_terminates (R: rel) s
: normal R s → terminates R s.
Relational approximation
Definition rle (R R´ : rel) :=
∀ x y, R x y → R´ x y.
Definition req (R R´ : rel) :=
(rle R R´ × rle R´ R)%type.
Reduction decidability
Definition reddec R :=
∀ x, reducible R x ∨ normal R x.
End Relations.
Global Hint Unfold symmetric transitive functional reducible normal total.
Require Import Omega.
Lemma complete_induction (p : nat → Prop) (x : nat)
: (∀ x, (∀ y, y<x → p y) → p x) → p x.
Lemma gt_terminates
: terminating gt.
Lemma size_induction (X : Type) (f : X → nat) (p: X →Prop) (x : X)
: (∀ x, (∀ y, f y < f x → p y) → p x) → p x.
Definition size_recursion (X : Type) (f : X → nat) (p: X → Type) (x : X)
: (∀ x, (∀ y, f y < f x → p y) → p x) → p x.
Inductive fstNoneOrR {X Y:Type} (R:X→Y→Prop)
: option X → option Y → Prop :=
| fstNone (x:option Y) : fstNoneOrR R None x
| bothR (x:X) (y:Y) : R x y → fstNoneOrR R (Some x) (Some y)
.
Instance fstNoneOrR_Reflexive {A : Type} {R : relation A} {Rrefl: Reflexive R}
: Reflexive (fstNoneOrR R).