diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-30 19:16:00 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-30 19:16:00 -0500 |
commit | 922e467dc432d630f83dfcd20c33f1eeb184d87b (patch) | |
tree | e12c6b57a27257f91bb9dff3672c5176d1411f6b | |
parent | 7f9164f563f5306bcbf487b61e252a258feb0476 (diff) |
Add Util.Sumbool
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Util/Sum.v | 60 | ||||
-rw-r--r-- | src/Util/Sumbool.v | 65 |
3 files changed, 126 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 0350d7016..3722bd752 100644 --- a/_CoqProject +++ b/_CoqProject @@ -394,6 +394,7 @@ src/Util/Prod.v src/Util/Relations.v src/Util/Sigma.v src/Util/Sum.v +src/Util/Sumbool.v src/Util/Tactics.v src/Util/Tower.v src/Util/Tuple.v diff --git a/src/Util/Sum.v b/src/Util/Sum.v index 51d52b12d..0bed606c2 100644 --- a/src/Util/Sum.v +++ b/src/Util/Sum.v @@ -1,6 +1,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.GlobalSettings. Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B) := fun x y => match x, y with @@ -32,3 +33,62 @@ Global Instance dec_sumwise {A B RA RB} {HA : DecidableRel RA} {HB : DecidableRe Proof. intros [x|x] [y|y]; exact _. Qed. + +(** ** Equality for [sum] *) +Section sum. + Local Notation sum_code u v + := (match u, v with + | inl u', inl v' + | inr u', inr v' + => u' = v' + | inl _, _ + | inr _, _ + => False + end). + + (** *** Equality of [sum] is a [match] *) + Definition path_sum {A B} (u v : sum A B) (p : sum_code u v) + : u = v. + Proof. destruct u, v; first [ apply f_equal | exfalso ]; exact p. Defined. + + (** *** Equivalence of equality of [sum] with [sum_code] *) + Definition unpath_sum {A B} {u v : sum A B} (p : u = v) + : sum_code u v. + Proof. subst v; destruct u; reflexivity. Defined. + + Definition path_sum_iff {A B} + (u v : @sum A B) + : u = v <-> sum_code u v. + Proof. + split; [ apply unpath_sum | apply path_sum ]. + Defined. + + (** *** Eta-expansion of [@eq (sum _ _)] *) + Definition path_sum_eta {A B} {u v : @sum A B} (p : u = v) + : p = path_sum u v (unpath_sum p). + Proof. destruct u, p; reflexivity. Defined. + + (** *** Induction principle for [@eq (sum _ _)] *) + Definition path_sum_rect {A B} {u v : @sum A B} (P : u = v -> Type) + (f : forall p, P (path_sum u v p)) + : forall p, P p. + Proof. intro p; specialize (f (unpath_sum p)); destruct u, p; exact f. Defined. + Definition path_sum_rec {A B u v} (P : u = v :> @sum A B -> Set) := path_sum_rect P. + Definition path_sum_ind {A B u v} (P : u = v :> @sum A B -> Prop) := path_sum_rec P. +End sum. + +(** ** Useful Tactics *) +(** *** [inversion_sum] *) +Ltac induction_path_sum H := + induction H as [H] using path_sum_rect; + try match type of H with + | False => exfalso; exact H + end. +Ltac inversion_sum_step := + match goal with + | [ H : _ = sum _ _ |- _ ] + => induction_path_sum H + | [ H : sum _ _ = _ |- _ ] + => induction_path_sum H + end. +Ltac inversion_sum := repeat inversion_sum_step. diff --git a/src/Util/Sumbool.v b/src/Util/Sumbool.v new file mode 100644 index 000000000..a21777605 --- /dev/null +++ b/src/Util/Sumbool.v @@ -0,0 +1,65 @@ +(** * Classification of the [{_} + {_}] Type *) +(** In this file, we classify the basic structure of [sumbool] types. *) +Require Import Crypto.Util.GlobalSettings. + +(*Local Set Keep Proof Equalities. +Scheme Equality for sumbool.*) + +(** ** Equality for [sumbool] *) +Section sumbool. + Local Notation sumbool_code u v + := (match u, v with + | left u', left v' + | right u', right v' + => u' = v' + | left _, _ + | right _, _ + => False + end). + + (** *** Equality of [sumbool] is a [match] *) + Definition path_sumbool {A B} (u v : sumbool A B) (p : sumbool_code u v) + : u = v. + Proof. destruct u, v; first [ apply f_equal | exfalso ]; exact p. Defined. + + (** *** Equivalence of equality of [sumbool] with [sumbool_code] *) + Definition unpath_sumbool {A B} {u v : sumbool A B} (p : u = v) + : sumbool_code u v. + Proof. subst v; destruct u; reflexivity. Defined. + + Definition path_sumbool_iff {A B} + (u v : @sumbool A B) + : u = v <-> sumbool_code u v. + Proof. + split; [ apply unpath_sumbool | apply path_sumbool ]. + Defined. + + (** *** Eta-expansion of [@eq (sumbool _ _)] *) + Definition path_sumbool_eta {A B} {u v : @sumbool A B} (p : u = v) + : p = path_sumbool u v (unpath_sumbool p). + Proof. destruct u, p; reflexivity. Defined. + + (** *** Induction principle for [@eq (sumbool _ _)] *) + Definition path_sumbool_rect {A B} {u v : @sumbool A B} (P : u = v -> Type) + (f : forall p, P (path_sumbool u v p)) + : forall p, P p. + Proof. intro p; specialize (f (unpath_sumbool p)); destruct u, p; exact f. Defined. + Definition path_sumbool_rec {A B u v} (P : u = v :> @sumbool A B -> Set) := path_sumbool_rect P. + Definition path_sumbool_ind {A B u v} (P : u = v :> @sumbool A B -> Prop) := path_sumbool_rec P. +End sumbool. + +(** ** Useful Tactics *) +(** *** [inversion_sumbool] *) +Ltac induction_path_sumbool H := + induction H as [H] using path_sumbool_rect; + try match type of H with + | False => exfalso; exact H + end. +Ltac inversion_sumbool_step := + match goal with + | [ H : _ = sumbool _ _ |- _ ] + => induction_path_sumbool H + | [ H : sumbool _ _ = _ |- _ ] + => induction_path_sumbool H + end. +Ltac inversion_sumbool := repeat inversion_sumbool_step. |