Commit e79e91f7 by Robbert Krebbers

### Add documentation, add license, simplify build process, some reorganization,

`improve some definitions, simplify some proofs.`
parent fb763df2
 Require Export base. Definition red `(R : relation A) (x : A) := ∃ y, R x y. Definition nf `(R : relation A) (x : A) := ¬red R x. (* The reflexive transitive closure *) Inductive rtc `(R : relation A) : relation A := | rtc_refl x : rtc R x x | rtc_l x y z : R x y → rtc R y z → rtc R x z. (* A reduction of exactly n steps *) Inductive nsteps `(R : relation A) : nat → relation A := | nsteps_O x : nsteps R 0 x x | nsteps_l n x y z : R x y → nsteps R n y z → nsteps R (S n) x z. (* A reduction whose length is bounded by n *) Inductive bsteps `(R : relation A) : nat → relation A := | bsteps_refl n x : bsteps R n x x | bsteps_l n x y z : R x y → bsteps R n y z → bsteps R (S n) x z. (* The transitive closure *) Inductive tc `(R : relation A) : relation A := | tc_once x y : R x y → tc R x y | tc_l x y z : R x y → tc R y z → tc R x z. Hint Constructors rtc nsteps bsteps tc : trs. Arguments rtc_l {_ _ _ _ _} _ _. Arguments nsteps_l {_ _ _ _ _ _} _ _. Arguments bsteps_refl {_ _} _ _. Arguments bsteps_l {_ _ _ _ _ _} _ _. Arguments tc_once {_ _ _} _ _. Arguments tc_l {_ _ _ _ _} _ _. Ltac generalize_rtc H := match type of H with | rtc ?R ?x ?y => let Hx := fresh in let Hy := fresh in let Heqx := fresh in let Heqy := fresh in remember x as (Hx,Heqx); remember y as (Hy,Heqy); revert Heqx Heqy; repeat match x with | context [ ?z ] => revert z end; repeat match y with | context [ ?z ] => revert z end end. (* Copyright (c) 2012, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** 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. This file defines a hint database [ars] containing some theorems on abstract rewriting systems. *) Require Export tactics base. (** * Definitions *) Section definitions. Context `(R : relation A). (** An element is reducible if a step is possible. *) Definition red (x : A) := ∃ y, R x y. (** An element is in normal form if no further steps are possible. *) Definition nf (x : A) := ¬red x. (** The reflexive transitive closure. *) Inductive rtc : relation A := | rtc_refl x : rtc x x | rtc_l x y z : R x y → rtc y z → rtc x z. (** Reductions of exactly [n] steps. *) Inductive nsteps : nat → relation A := | nsteps_O x : nsteps 0 x x | nsteps_l n x y z : R x y → nsteps n y z → nsteps (S n) x z. (** Reduction of at most [n] steps. *) Inductive bsteps : nat → relation A := | bsteps_refl n x : bsteps n x x | bsteps_l n x y z : R x y → bsteps n y z → bsteps (S n) x z. (** The transitive closure. *) Inductive tc : relation A := | tc_once x y : R x y → tc x y | tc_l x y z : R x y → tc y z → tc x z. (** An element [x] is looping if all paths starting at [x] are infinite. *) CoInductive looping : A → Prop := | looping_do_step x : red x → (∀ y, R x y → looping y) → looping x. End definitions. Hint Constructors rtc nsteps bsteps tc : ars. (** * General theorems *) Section rtc. Context `{R : relation A}. Global Instance: Reflexive (rtc R). Proof rtc_refl R. Global Instance rtc_trans: Transitive (rtc R). Proof. red; induction 1; eauto with trs. Qed. Lemma rtc_once {x y} : R x y → rtc R x y. Proof. eauto with trs. Qed. Proof. red; induction 1; eauto with ars. Qed. Lemma rtc_once x y : R x y → rtc R x y. Proof. eauto with ars. Qed. Global Instance: subrelation R (rtc R). Proof. exact @rtc_once. Qed. Lemma rtc_r {x y z} : rtc R x y → R y z → rtc R x z. Proof. intros. etransitivity; eauto with trs. Qed. Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z. Proof. intros. etransitivity; eauto with ars. Qed. Lemma rtc_inv {x z} : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z. Lemma rtc_inv x z : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z. Proof. inversion_clear 1; eauto. Qed. Lemma rtc_ind_r (P : A → A → Prop) Lemma rtc_ind_r (P : A → A → Prop) (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) : ∀ y z, rtc R y z → P y z. Proof. ... ... @@ -70,58 +70,76 @@ Section rtc. induction 1; eauto using rtc_r. Qed. Lemma rtc_inv_r {x z} : rtc R x z → x = z ∨ ∃ y, rtc R x y ∧ R y z. Lemma rtc_inv_r x z : rtc R x z → x = z ∨ ∃ y, rtc R x y ∧ R y z. Proof. revert x z. apply rtc_ind_r; eauto. Qed. Lemma nsteps_once {x y} : R x y → nsteps R 1 x y. Proof. eauto with trs. Qed. Lemma nsteps_trans {n m x y z} : Lemma nsteps_once x y : R x y → nsteps R 1 x y. Proof. eauto with ars. Qed. Lemma nsteps_trans n m x y z : nsteps R n x y → nsteps R m y z → nsteps R (n + m) x z. Proof. induction 1; simpl; eauto with trs. Qed. Lemma nsteps_r {n x y z} : nsteps R n x y → R y z → nsteps R (S n) x z. Proof. induction 1; eauto with trs. Qed. Lemma nsteps_rtc {n x y} : nsteps R n x y → rtc R x y. Proof. induction 1; eauto with trs. Qed. Lemma rtc_nsteps {x y} : rtc R x y → ∃ n, nsteps R n x y. Proof. induction 1; firstorder eauto with trs. Qed. Lemma bsteps_once {n x y} : R x y → bsteps R (S n) x y. Proof. eauto with trs. Qed. Lemma bsteps_plus_r {n m x y} : Proof. induction 1; simpl; eauto with ars. Qed. Lemma nsteps_r n x y z : nsteps R n x y → R y z → nsteps R (S n) x z. Proof. induction 1; eauto with ars. Qed. Lemma nsteps_rtc n x y : nsteps R n x y → rtc R x y. Proof. induction 1; eauto with ars. Qed. Lemma rtc_nsteps x y : rtc R x y → ∃ n, nsteps R n x y. Proof. induction 1; firstorder eauto with ars. Qed. Lemma bsteps_once n x y : R x y → bsteps R (S n) x y. Proof. eauto with ars. Qed. Lemma bsteps_plus_r n m x y : bsteps R n x y → bsteps R (n + m) x y. Proof. induction 1; simpl; eauto with trs. Qed. Lemma bsteps_weaken {n m x y} : Proof. induction 1; simpl; eauto with ars. Qed. Lemma bsteps_weaken n m x y : n ≤ m → bsteps R n x y → bsteps R m x y. Proof. intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r. Qed. Lemma bsteps_plus_l {n m x y} : Lemma bsteps_plus_l n m x y : bsteps R n x y → bsteps R (m + n) x y. Proof. apply bsteps_weaken. auto with arith. Qed. Lemma bsteps_S {n x y} : bsteps R n x y → bsteps R (S n) x y. Lemma bsteps_S n x y : bsteps R n x y → bsteps R (S n) x y. Proof. apply bsteps_weaken. auto with arith. Qed. Lemma bsteps_trans {n m x y z} : Lemma bsteps_trans n m x y z : bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z. Proof. induction 1; simpl; eauto using bsteps_plus_l with trs. Qed. Lemma bsteps_r {n x y z} : bsteps R n x y → R y z → bsteps R (S n) x z. Proof. induction 1; eauto with trs. Qed. Lemma bsteps_rtc {n x y} : bsteps R n x y → rtc R x y. Proof. induction 1; eauto with trs. Qed. Lemma rtc_bsteps {x y} : rtc R x y → ∃ n, bsteps R n x y. Proof. induction 1. exists 0. auto with trs. firstorder eauto with trs. Qed. Proof. induction 1; simpl; eauto using bsteps_plus_l with ars. Qed. Lemma bsteps_r n x y z : bsteps R n x y → R y z → bsteps R (S n) x z. Proof. induction 1; eauto with ars. Qed. Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y. Proof. induction 1; eauto with ars. Qed. Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y. Proof. induction 1. exists 0. auto with ars. firstorder eauto with ars. Qed. Global Instance tc_trans: Transitive (tc R). Proof. red; induction 1; eauto with trs. Qed. Lemma tc_r {x y z} : tc R x y → R y z → tc R x z. Proof. intros. etransitivity; eauto with trs. Qed. Lemma tc_rtc {x y} : tc R x y → rtc R x y. Proof. induction 1; eauto with trs. Qed. Proof. red; induction 1; eauto with ars. Qed. Lemma tc_r x y z : tc R x y → R y z → tc R x z. Proof. intros. etransitivity; eauto with ars. Qed. Lemma tc_rtc x y : tc R x y → rtc R x y. Proof. induction 1; eauto with ars. Qed. Global Instance: subrelation (tc R) (rtc R). Proof. exact @tc_rtc. Qed. Lemma looping_red x : looping R x → red R x. Proof. destruct 1; auto. Qed. Lemma looping_step x y : looping R x → R x y → looping R y. Proof. destruct 1; auto. Qed. Lemma looping_rtc x y : looping R x → rtc R x y → looping R y. Proof. induction 2; eauto using looping_step. Qed. Lemma looping_alt x : looping R x ↔ ∀ y, rtc R x y → red R y. Proof. split. * eauto using looping_red, looping_rtc. * intros H. cut (∀ z, rtc R x z → looping R z). { eauto with ars. } cofix FIX. constructor; eauto using rtc_r with ars. Qed. End rtc. Hint Resolve rtc_once rtc_r tc_r : trs. Hint Resolve rtc_once rtc_r tc_r : ars. (** * Theorems on sub relations *) Section subrel. Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2). ... ...
This diff is collapsed.
This diff is collapsed.
 (* Copyright (c) 2012, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects theorems, definitions, tactics, related to propositions with a decidable equality. Such propositions are collected by the [Decision] type class. *) Require Export base. Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x y)} (x : A) (y : B) : Decision (R x y) := dec x y. (** We introduce [decide_rel] to avoid inefficienct computation due to eager evaluation of propositions by [vm_compute]. This inefficiency occurs if [(x = y) := (f x = f y)] as [decide (x = y)] evaluates to [decide (f x = f y)] which then might lead to evaluation of [f x] and [f y]. Using [decide_rel] we hide [f] under a lambda abstraction to avoid this unnecessary evaluation. *) Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x y)} (x : A) (y : B) : Decision (R x y) := dec x y. Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y)} (x : A) (y : B) : decide_rel R x y = decide (R x y). Proof. easy. Qed. Ltac case_decide := (** The tactic [case_decide] performs case analysis on an arbitrary occurrence of [decide] or [decide_rel] in the conclusion or assumptions. *) Ltac case_decide := match goal with | H : context [@decide ?P ?dec] |- _ => case (@decide P dec) in * | H : context [@decide ?P ?dec] |- _ => destruct (@decide P dec) | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => case (@decide_rel _ _ R x y dec) in * | |- context [@decide ?P ?dec] => case (@decide P dec) in * destruct (@decide_rel _ _ R x y dec) | |- context [@decide ?P ?dec] => destruct (@decide P dec) | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => case (@decide_rel _ _ R x y dec) in * destruct (@decide_rel _ _ R x y dec) end. (** The tactic [solve_decision] uses Coq's [decide equality] tactic together with instance resolution to automatically generate decision procedures. *) Ltac solve_trivial_decision := match goal with | [ |- Decision (?P) ] => apply _ | [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _ end. Ltac solve_decision := Ltac solve_decision := intros; first [ solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision ]. Program Instance True_dec: Decision True := left _. Program Instance False_dec: Decision False := right _. Program Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y)) `(B_dec : ∀ x y : B, Decision (x = y)) : ∀ x y : A * B, Decision (x = y) := λ x y, match A_dec (fst x) (fst y) with | left _ => match B_dec (snd x) (snd y) with left _ => left _ | right _ => right _ end | right _ => right _ end. Solve Obligations using (program_simpl; f_equal; firstorder). Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∧ Q) := match P_dec with | left _ => match Q_dec with left _ => left _ | right _ => right _ end | right _ => right _ end. Solve Obligations using (program_simpl; tauto). Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∨ Q) := match P_dec with | left _ => left _ | right _ => match Q_dec with left _ => left _ | right _ => right _ end end. Solve Obligations using (program_simpl; firstorder). (** We can convert decidable propositions to booleans. *) Definition bool_decide (P : Prop) {dec : Decision P} : bool := if dec then true else false. Definition bool_decide (P : Prop) {dec : Decision P} : bool := if dec then true else false. Coercion Is_true : bool >-> Sortclass. Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P. Proof. unfold bool_decide. now destruct dec. Qed. Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P. Proof. unfold bool_decide. now destruct dec. Qed. (** * Decidable Sigma types *) (** Leibniz equality on Sigma types requires the equipped proofs to be equal as Coq does not support proof irrelevance. For decidable we propositions we define the type [dsig P] whose Leibniz equality is proof irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *) Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} := { x | bool_decide (P x) }. Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) := ... ... @@ -60,15 +62,46 @@ Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) := Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P := x↾bool_decide_pack _ p. Lemma proj1_dsig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) : x↾Px = y↾Py → x = y. Proof. now injection 1. Qed. Lemma dsig_eq {A} (P : A → Prop) {dec : ∀ x, Decision (P x)} (x y : { x | bool_decide (P x) }) : `x = `y → x = y. (x y : dsig P) : x = y ↔ `x = `y. Proof. intros H1. destruct x as [x Hx], y as [y Hy]. simpl in *. subst. f_equal. revert Hx Hy. case (bool_decide (P y)). * now intros [] []. * easy. split. * destruct x, y. apply proj1_sig_inj. * intro. destruct x as [x Hx], y as [y Hy]. simpl in *. subst. f_equal. revert Hx Hy. case (bool_decide (P y)). + now intros [] []. + easy. Qed. (** * Instances of Decision *) (** Instances of [Decision] for operators of propositional logic. *) Program Instance True_dec: Decision True := left _. Program Instance False_dec: Decision False := right _. Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∧ Q) := match P_dec with | left _ => match Q_dec with left _ => left _ | right _ => right _ end | right _ => right _ end. Solve Obligations using intuition. Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∨ Q) := match P_dec with | left _ => left _ | right _ => match Q_dec with left _ => left _ | right _ => right _ end end. Solve Obligations using intuition. (** Instances of [Decision] for common data types. *) Program Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y)) `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y) := match A_dec (fst x) (fst y) with | left _ => match B_dec (snd x) (snd y) with | left _ => left _ | right _ => right _ end | right _ => right _ end. Solve Obligations using intuition (simpl;congruence).