Commit e82cda6c authored by Robbert Krebbers's avatar Robbert Krebbers

Add non-deterministic expressions with side-effects.

The following things have been changed in this revision:

* We now give a small step semantics for expressions. The denotational semantics
  only works for side-effect free expressions.
* Dynamically allocated memory through alloc and free is now supported.
* The following expressions are added: assignment, function call, unary
  operators, conditional, alloc, and free.
* Some customary induction schemes for expressions are proven.
* The axiomatic semantics (and its interpretation) have been changed in order
  to deal with non-deterministic expressions.
* We have added inversion schemes based on small inversions for the operational
  semantics. Inversions using these schemes are much faster.
* We improved the statement preservation proof of the operational semantics.
* We now use a variant of SsReflect's [by] and [done], instead of Coq's [now]
  and [easy]. The [done] tactic is much faster as it does not perform
  inversions.
* Add theory, definitions and notations on vectors.
* Separate theory on contexts.
* Change [Arguments] declarations to ensure better unfolding.
parent 4cda26dd
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
These are particularly useful as we define the operational semantics as a These are particularly useful as we define the operational semantics as a
small step semantics. This file defines a hint database [ars] containing small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *) some theorems on abstract rewriting systems. *)
Require Import Omega Wf_nat.
Require Export tactics base. Require Export tactics base.
(** * Definitions *) (** * Definitions *)
...@@ -62,8 +63,9 @@ Section rtc. ...@@ -62,8 +63,9 @@ Section rtc.
Proof. inversion_clear 1; eauto. Qed. 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) : (Prefl : x, P x x)
y z, rtc R y z P y z. (Pstep : x y z, rtc R x y R y z P x y P x z) :
x z, rtc R x z P x z.
Proof. Proof.
cut ( y z, rtc R y z x, rtc R x y P x y P x z). cut ( y z, rtc R y z x, rtc R x y P x y P x z).
{ eauto using rtc_refl. } { eauto using rtc_refl. }
...@@ -99,7 +101,7 @@ Section rtc. ...@@ -99,7 +101,7 @@ Section rtc.
bsteps R n x y bsteps R (m + n) x y. bsteps R n x y bsteps R (m + n) x y.
Proof. apply bsteps_weaken. auto with arith. Qed. 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. Proof. apply bsteps_weaken. omega. 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. 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 ars. Qed. Proof. induction 1; simpl; eauto using bsteps_plus_l with ars. Qed.
...@@ -108,7 +110,31 @@ Section rtc. ...@@ -108,7 +110,31 @@ Section rtc.
Lemma bsteps_rtc n x y : bsteps R n x y rtc R x y. Lemma bsteps_rtc n x y : bsteps R n x y rtc R x y.
Proof. induction 1; eauto with ars. Qed. Proof. induction 1; eauto with ars. Qed.
Lemma rtc_bsteps x y : rtc R x y n, bsteps R n x y. 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. Proof.
induction 1.
* exists 0. constructor.
* naive_solver eauto with ars.
Qed.
Lemma bsteps_ind_r (P : nat A Prop) (x : A)
(Prefl : n, P n x)
(Pstep : n y z, bsteps R n x y R y z P n y P (S n) z) :
n z, bsteps R n x z P n z.
Proof.
cut ( m y z, bsteps R m y z n,
bsteps R n x y
( m', n m' m' n + m P m' y)
P (n + m) z).
{ intros help ?. change n with (0 + n). eauto with ars. }
induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
intros n p1 H. rewrite <-plus_n_Sm.
apply (IH (S n)); [by eauto using bsteps_r |].
intros [|m'] [??]; [omega |].
apply Pstep with x'.
* apply bsteps_weaken with n; intuition omega.
* done.
* apply H; intuition omega.
Qed.
Global Instance tc_trans: Transitive (tc R). Global Instance tc_trans: Transitive (tc R).
Proof. red; induction 1; eauto with ars. Qed. Proof. red; induction 1; eauto with ars. Qed.
...@@ -137,23 +163,26 @@ Section rtc. ...@@ -137,23 +163,26 @@ Section rtc.
Qed. Qed.
End rtc. End rtc.
Hint Resolve rtc_once rtc_r tc_r : ars. Hint Resolve
rtc_once rtc_r
tc_r
bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.
(** * Theorems on sub relations *) (** * Theorems on sub relations *)
Section subrel. Section subrel.
Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2). Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2).
Lemma red_subrel x : red R1 x red R2 x. Lemma red_subrel x : red R1 x red R2 x.
Proof. intros [y ?]. exists y. now apply Hsub. Qed. Proof. intros [y ?]. exists y. by apply Hsub. Qed.
Lemma nf_subrel x : nf R2 x nf R1 x. Lemma nf_subrel x : nf R2 x nf R1 x.
Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed. Proof. intros H1 H2. destruct H1. by apply red_subrel. Qed.
Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2). Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n). Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n). Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
Global Instance tc_subrel: subrelation (tc R1) (tc R2). Global Instance tc_subrel: subrelation (tc R1) (tc R2).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
End subrel. End subrel.
This diff is collapsed.
...@@ -7,59 +7,108 @@ Require Export base tactics orders. ...@@ -7,59 +7,108 @@ Require Export base tactics orders.
(** * Theorems *) (** * Theorems *)
Section collection. Section collection.
Context `{Collection A B}. Context `{Collection A C}.
Lemma elem_of_empty x : x False. Lemma elem_of_empty x : x False.
Proof. split. apply not_elem_of_empty. easy. Qed. Proof. split. apply not_elem_of_empty. done. Qed.
Lemma elem_of_union_l x X Y : x X x X Y. Lemma elem_of_union_l x X Y : x X x X Y.
Proof. intros. apply elem_of_union. auto. Qed. Proof. intros. apply elem_of_union. auto. Qed.
Lemma elem_of_union_r x X Y : x Y x X Y. Lemma elem_of_union_r x X Y : x Y x X Y.
Proof. intros. apply elem_of_union. auto. Qed. Proof. intros. apply elem_of_union. auto. Qed.
Lemma not_elem_of_singleton x y : x {[ y ]} x y.
Proof. now rewrite elem_of_singleton. Qed.
Lemma not_elem_of_union x X Y : x X Y x X x Y.
Proof. rewrite elem_of_union. tauto. Qed.
Global Instance collection_subseteq: SubsetEq B := λ X Y, Global Instance collection_subseteq: SubsetEq C := λ X Y,
x, x X x Y. x, x X x Y.
Global Instance: BoundedJoinSemiLattice B. Global Instance: LowerBoundedLattice C.
Proof. firstorder. Qed. Proof. firstorder auto. Qed.
Global Instance: MeetSemiLattice B.
Proof. firstorder. Qed.
Lemma elem_of_subseteq X Y : X Y x, x X x Y. Lemma elem_of_subseteq X Y : X Y x, x X x Y.
Proof. easy. Qed. Proof. done. Qed.
Lemma elem_of_equiv X Y : X Y x, x X x Y. Lemma elem_of_equiv X Y : X Y x, x X x Y.
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma elem_of_equiv_alt X Y : Lemma elem_of_equiv_alt X Y :
X Y ( x, x X x Y) ( x, x Y x X). X Y ( x, x X x Y) ( x, x Y x X).
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma elem_of_subseteq_singleton x X : x X {[ x ]} X.
Proof.
split.
* intros ??. rewrite elem_of_singleton. intro. by subst.
* intros Ex. by apply (Ex x), elem_of_singleton.
Qed.
Global Instance singleton_proper : Proper ((=) ==> ()) singleton. Global Instance singleton_proper : Proper ((=) ==> ()) singleton.
Proof. repeat intro. now subst. Qed. Proof. repeat intro. by subst. Qed.
Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) (). Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) ().
Proof. intros ???. subst. firstorder. Qed. Proof. intros ???. subst. firstorder. Qed.
Lemma empty_ne_singleton x : {[ x ]}. Lemma elem_of_union_list (x : A) (Xs : list C) :
x Xs X, In X Xs x X.
Proof.
split.
* induction Xs; simpl; intros HXs.
+ by apply elem_of_empty in HXs.
+ apply elem_of_union in HXs. naive_solver.
* intros [X []]. induction Xs; [done | intros [?|?] ?; subst; simpl].
+ by apply elem_of_union_l.
+ apply elem_of_union_r; auto.
Qed.
Lemma non_empty_singleton x : {[ x ]} .
Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
Lemma intersection_twice x : {[x]} {[x]} {[x]}.
Proof. Proof.
intros [_ E]. apply (elem_of_empty x). split; intros y; rewrite elem_of_intersection, !elem_of_singleton; tauto.
apply E. now apply elem_of_singleton. Qed.
Lemma not_elem_of_singleton x y : x {[ y ]} x y.
Proof. by rewrite elem_of_singleton. Qed.
Lemma not_elem_of_union x X Y : x X Y x X x Y.
Proof. rewrite elem_of_union. tauto. Qed.
Context `{ (X Y : C), Decision (X Y)}.
Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x X) | 100.
Proof.
refine (cast_if (decide_rel () {[ x ]} X));
by rewrite elem_of_subseteq_singleton.
Defined.
Lemma not_elem_of_intersection x X Y : x X Y x X x Y.
Proof.
rewrite elem_of_intersection.
destruct (decide (x X)); tauto.
Qed.
Lemma not_elem_of_difference x X Y : x X Y x X x Y.
Proof.
rewrite elem_of_difference.
destruct (decide (x Y)); tauto.
Qed.
Lemma union_difference X Y : X Y X X Y.
Proof.
split; intros x; rewrite !elem_of_union, elem_of_difference.
* tauto.
* destruct (decide (x X)); tauto.
Qed. Qed.
End collection. End collection.
Ltac decompose_empty := repeat
match goal with
| H : _ _ |- _ => apply empty_union in H; destruct H
| H : _ _ |- _ => apply non_empty_union in H; destruct H
| H : {[ _ ]} |- _ => destruct (non_empty_singleton _ H)
end.
(** * Theorems about map *) (** * Theorems about map *)
Section map. Section map.
Context `{Collection A C}. Context `{Collection A C}.
Lemma elem_of_map_1 (f : A A) (X : C) (x : A) : Lemma elem_of_map_1 (f : A A) (X : C) (x : A) :
x map f X y, x = f y y X.
Proof. intros. by apply (elem_of_map _). Qed.
Lemma elem_of_map_2 (f : A A) (X : C) (x : A) :
x X f x map f X. x X f x map f X.
Proof. intros. apply (elem_of_map _). eauto. Qed. Proof. intros. apply (elem_of_map _). eauto. Qed.
Lemma elem_of_map_1_alt (f : A A) (X : C) (x : A) y : Lemma elem_of_map_2_alt (f : A A) (X : C) (x : A) y :
x X y = f x y map f X. x X y = f x y map f X.
Proof. intros. apply (elem_of_map _). eauto. Qed. Proof. intros. apply (elem_of_map _). eauto. Qed.
Lemma elem_of_map_2 (f : A A) (X : C) (x : A) :
x map f X y, x = f y y X.
Proof. intros. now apply (elem_of_map _). Qed.
End map. End map.
(** * Tactics *) (** * Tactics *)
...@@ -67,16 +116,19 @@ End map. ...@@ -67,16 +116,19 @@ End map.
[(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into [(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into
logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into
[A → x ∈ X ∨ False]. *) [A → x ∈ X ∨ False]. *)
Ltac unfold_elem_of := repeat Ltac unfold_elem_of :=
match goal with repeat_on_hyps (fun H =>
| H : context [ _ _ ] |- _ => setoid_rewrite elem_of_subseteq in H repeat match type of H with
| H : context [ _ _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H | context [ _ _ ] => setoid_rewrite elem_of_subseteq in H
| H : context [ _ ] |- _ => setoid_rewrite elem_of_empty in H | context [ _ _ ] => setoid_rewrite elem_of_equiv_alt in H
| H : context [ _ {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H | context [ _ ] => setoid_rewrite elem_of_empty in H
| H : context [ _ _ _ ] |- _ => setoid_rewrite elem_of_union in H | context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
| H : context [ _ _ _ ] |- _ => setoid_rewrite elem_of_intersection in H | context [ _ _ _ ] => setoid_rewrite elem_of_union in H
| H : context [ _ _ _ ] |- _ => setoid_rewrite elem_of_difference in H | context [ _ _ _ ] => setoid_rewrite elem_of_intersection in H
| H : context [ _ map _ _ ] |- _ => setoid_rewrite elem_of_map in H | context [ _ _ _ ] => setoid_rewrite elem_of_difference in H
| context [ _ map _ _ ] => setoid_rewrite elem_of_map in H
end);
repeat match goal with
| |- context [ _ _ ] => setoid_rewrite elem_of_subseteq | |- context [ _ _ ] => setoid_rewrite elem_of_subseteq
| |- context [ _ _ ] => setoid_rewrite elem_of_equiv_alt | |- context [ _ _ ] => setoid_rewrite elem_of_equiv_alt
| |- context [ _ ] => setoid_rewrite elem_of_empty | |- context [ _ ] => setoid_rewrite elem_of_empty
...@@ -90,7 +142,7 @@ Ltac unfold_elem_of := repeat ...@@ -90,7 +142,7 @@ Ltac unfold_elem_of := repeat
(** The tactic [solve_elem_of tac] composes the above tactic with [intuition]. (** The tactic [solve_elem_of tac] composes the above tactic with [intuition].
For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is
generally powerful enough. This tactic either fails or proves the goal. *) generally powerful enough. This tactic either fails or proves the goal. *)
Tactic Notation "solve_elem_of" tactic(tac) := Tactic Notation "solve_elem_of" tactic3(tac) :=
simpl in *; simpl in *;
unfold_elem_of; unfold_elem_of;
solve [intuition (simplify_equality; tac)]. solve [intuition (simplify_equality; tac)].
...@@ -101,19 +153,20 @@ Tactic Notation "solve_elem_of" := solve_elem_of auto. ...@@ -101,19 +153,20 @@ Tactic Notation "solve_elem_of" := solve_elem_of auto.
fails or loops on very small goals generated by [solve_elem_of] already. We fails or loops on very small goals generated by [solve_elem_of] already. We
use the [naive_solver] tactic as a substitute. This tactic either fails or use the [naive_solver] tactic as a substitute. This tactic either fails or
proves the goal. *) proves the goal. *)
Tactic Notation "esolve_elem_of" tactic(tac) := Tactic Notation "esolve_elem_of" tactic3(tac) :=
simpl in *; simpl in *;
unfold_elem_of; unfold_elem_of;
naive_solver tac. naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.
(** Given an assumption [H : _ ∈ _], the tactic [destruct_elem_of H] will (** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will
recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *) recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *)
Tactic Notation "destruct_elem_of" hyp(H) := Tactic Notation "decompose_elem_of" hyp(H) :=
let rec go H := let rec go H :=
lazymatch type of H with lazymatch type of H with
| _ => apply elem_of_empty in H; destruct H | _ => apply elem_of_empty in H; destruct H
| _ {[ ?l' ]} => apply elem_of_singleton in H; subst l' | ?l {[ ?l' ]} =>
apply elem_of_singleton in H; first [ subst l' | subst l | idtac ]
| _ _ _ => | _ _ _ =>
let H1 := fresh in let H2 := fresh in apply elem_of_union in H; let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
destruct H as [H1|H2]; [go H1 | go H2] destruct H as [H1|H2]; [go H1 | go H2]
...@@ -128,6 +181,8 @@ Tactic Notation "destruct_elem_of" hyp(H) := ...@@ -128,6 +181,8 @@ Tactic Notation "destruct_elem_of" hyp(H) :=
destruct H as [?[? H1]]; go H1 destruct H as [?[? H1]]; go H1
| _ => idtac | _ => idtac
end in go H. end in go H.
Tactic Notation "decompose_elem_of" :=
repeat_on_hyps (fun H => decompose_elem_of H).
(** * Sets without duplicates up to an equivalence *) (** * Sets without duplicates up to an equivalence *)
Section no_dup. Section no_dup.
...@@ -208,10 +263,10 @@ End quantifiers. ...@@ -208,10 +263,10 @@ End quantifiers.
Section more_quantifiers. Section more_quantifiers.
Context `{Collection A B}. Context `{Collection A B}.
Lemma cforall_weak (P Q : A Prop) (Hweak : x, P x Q x) X : Lemma cforall_weaken (P Q : A Prop) (Hweaken : x, P x Q x) X :
cforall P X cforall Q X. cforall P X cforall Q X.
Proof. unfold cforall. naive_solver. Qed. Proof. unfold cforall. naive_solver. Qed.
Lemma cexists_weak (P Q : A Prop) (Hweak : x, P x Q x) X : Lemma cexists_weaken (P Q : A Prop) (Hweaken : x, P x Q x) X :
cexists P X cexists Q X. cexists P X cexists Q X.
Proof. unfold cexists. naive_solver. Qed. Proof. unfold cexists. naive_solver. Qed.
End more_quantifiers. End more_quantifiers.
...@@ -226,7 +281,7 @@ Section fresh. ...@@ -226,7 +281,7 @@ Section fresh.
exist ( X) (fresh X) (is_fresh X). exist ( X) (fresh X) (is_fresh X).
Global Instance fresh_proper: Proper (() ==> (=)) fresh. Global Instance fresh_proper: Proper (() ==> (=)) fresh.
Proof. intros ???. now apply fresh_proper_alt, elem_of_equiv. Qed. Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
Fixpoint fresh_list (n : nat) (X : C) : list A := Fixpoint fresh_list (n : nat) (X : C) : list A :=
match n with match n with
...@@ -238,8 +293,8 @@ Section fresh. ...@@ -238,8 +293,8 @@ Section fresh.
Proof. Proof.
intros ? n ?. subst. intros ? n ?. subst.
induction n; simpl; intros ?? E; f_equal. induction n; simpl; intros ?? E; f_equal.
* now rewrite E. * by rewrite E.
* apply IHn. now rewrite E. * apply IHn. by rewrite E.
Qed. Qed.
Lemma fresh_list_length n X : length (fresh_list n X) = n. Lemma fresh_list_length n X : length (fresh_list n X) = n.
...@@ -248,7 +303,7 @@ Section fresh. ...@@ -248,7 +303,7 @@ Section fresh.
Lemma fresh_list_is_fresh n X x : In x (fresh_list n X) x X. Lemma fresh_list_is_fresh n X x : In x (fresh_list n X) x X.
Proof. Proof.
revert X. induction n; simpl. revert X. induction n; simpl.
* easy. * done.
* intros X [?| Hin]. subst. * intros X [?| Hin]. subst.
+ apply is_fresh. + apply is_fresh.
+ apply IHn in Hin. solve_elem_of. + apply IHn in Hin. solve_elem_of.
......
...@@ -3,7 +3,10 @@ ...@@ -3,7 +3,10 @@
(** This file collects theorems, definitions, tactics, related to propositions (** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision] with a decidable equality. Such propositions are collected by the [Decision]
type class. *) type class. *)
Require Export base. Require Export base tactics.
Lemma dec_stable `{Decision P} : ¬¬P P.
Proof. firstorder. Qed.
(** We introduce [decide_rel] to avoid inefficienct computation due to eager (** We introduce [decide_rel] to avoid inefficienct computation due to eager
evaluation of propositions by [vm_compute]. This inefficiency occurs if evaluation of propositions by [vm_compute]. This inefficiency occurs if
...@@ -14,10 +17,10 @@ Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x ...@@ -14,10 +17,10 @@ Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x
(x : A) (y : B) : Decision (R x y) := dec 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)} 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). (x : A) (y : B) : decide_rel R x y = decide (R x y).
Proof. easy. Qed. Proof. done. Qed.
(** The tactic [case_decide] performs case analysis on an arbitrary occurrence (** The tactic [case_decide] performs case analysis on an arbitrary occurrence
of [decide] or [decide_rel] in the conclusion or assumptions. *) of [decide] or [decide_rel] in the conclusion or hypotheses. *)
Ltac case_decide := Ltac case_decide :=
match goal with match goal with
| H : context [@decide ?P ?dec] |- _ => | H : context [@decide ?P ?dec] |- _ =>
...@@ -34,21 +37,21 @@ Ltac case_decide := ...@@ -34,21 +37,21 @@ Ltac case_decide :=
with instance resolution to automatically generate decision procedures. *) with instance resolution to automatically generate decision procedures. *)
Ltac solve_trivial_decision := Ltac solve_trivial_decision :=
match goal with match goal with
| [ |- Decision (?P) ] => apply _ | |- Decision (?P) => apply _
| [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _ | |- sumbool ?P (¬?P) => change (Decision P); apply _
end. end.
Ltac solve_decision := Ltac solve_decision := intros; first
intros; first [ solve_trivial_decision [ solve_trivial_decision
| unfold Decision; decide equality; solve_trivial_decision ]. | unfold Decision; decide equality; solve_trivial_decision ].
(** We can convert decidable propositions to booleans. *) (** We can convert decidable propositions to booleans. *)
Definition bool_decide (P : Prop) {dec : Decision P} : bool := Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
if dec then true else false. if dec then true else false.
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P P. Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P P.
Proof. unfold bool_decide. now destruct dec. Qed. Proof. unfold bool_decide. by destruct dec. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P. Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. unfold bool_decide. now destruct dec. Qed. Proof. unfold bool_decide. by destruct dec. Qed.
(** * Decidable Sigma types *) (** * Decidable Sigma types *)
(** Leibniz equality on Sigma types requires the equipped proofs to be (** Leibniz equality on Sigma types requires the equipped proofs to be
...@@ -70,38 +73,43 @@ Proof. ...@@ -70,38 +73,43 @@ Proof.
* intro. destruct x as [x Hx], y as [y Hy]. * intro. destruct x as [x Hx], y as [y Hy].
simpl in *. subst. f_equal. simpl in *. subst. f_equal.
revert Hx Hy. case (bool_decide (P y)). revert Hx Hy. case (bool_decide (P y)).
+ now intros [] []. + by intros [] [].
+ easy. + done.
Qed. Qed.
(** The following combinators are useful to create Decision proofs in
combination with the [refine] tactic. *)
Notation cast_if S := (if S then left _ else right _).
Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
Notation cast_if_not S := (if S then right _ else left _).
(** * Instances of Decision *) (** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *) (** Instances of [Decision] for operators of propositional logic. *)
Program Instance True_dec: Decision True := left _. Instance True_dec: Decision True := left I.
Program Instance False_dec: Decision False := right _. Instance False_dec: Decision False := right (False_rect False).
Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
Decision (P Q) := Section prop_dec.
match P_dec with Context `(P_dec : Decision P) `(Q_dec : Decision Q).
| left _ => match Q_dec with left _ => left _ | right _ => right _ end
| right _ => right _ Global Instance and_dec: Decision (P Q).
end. Proof. refine (cast_if_and P_dec Q_dec); intuition. Qed.
Solve Obligations using intuition.