diff options
author | Jason Gross <jagro@google.com> | 2016-09-05 11:54:43 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-09-05 11:54:43 -0700 |
commit | ed88b28433ef90f8be554803a4fe852a6634ee87 (patch) | |
tree | de6b2a2c050f0ed56f684e99f7e550a1cf485615 /src/Util/PointedProp.v | |
parent | fe4b156f34c8a0ac994ff4cdb40755d23bc5e7b9 (diff) |
Add a file about pointed Props
Diffstat (limited to 'src/Util/PointedProp.v')
-rw-r--r-- | src/Util/PointedProp.v | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/src/Util/PointedProp.v b/src/Util/PointedProp.v new file mode 100644 index 000000000..76c760632 --- /dev/null +++ b/src/Util/PointedProp.v @@ -0,0 +1,46 @@ +(** * Propositions with a distinguished point representing true *) +(** This allows for something between [bool] and [Prop], where we can + computationally reduce things like [True /\ True], but can still + express equality of types. *) +Require Import Crypto.Util.Notations. + +Delimit Scope pointed_prop_scope with pointed_prod. +Inductive pointed_Prop := trivial | inject (_ : Prop). +Bind Scope pointed_prop_scope with pointed_Prop. + +Definition to_prop (x : pointed_Prop) : Prop + := match x with + | trivial => True + | inject p => p + end. + +Definition and_pointed_Prop (x y : pointed_Prop) : pointed_Prop + := match x, y with + | trivial, y => y + | x, trivial => x + | inject p, inject q => inject (p /\ q) + end. + +Definition or_pointed_Prop (x y : pointed_Prop) : pointed_Prop + := match x, y with + | trivial, _ => trivial + | _, trivial => trivial + | inject p, inject q => inject (p \/ q) + end. + +Definition impl_pointed_Prop (x y : pointed_Prop) : pointed_Prop + := match x, y with + | trivial, y => y + | _, trivial => trivial + | inject p, inject q => inject (p -> q) + end. + +Infix "/\" := and_pointed_Prop : pointed_prop_scope. +Infix "\/" := or_pointed_Prop : pointed_prop_scope. +Infix "->" := impl_pointed_Prop : pointed_prop_scope. + +Ltac inversion_pointed_Prop_step := + match goal with + | [ H : inject _ = inject _ |- _ ] => progress (inversion H; clear H) + end. +Ltac inversion_pointed_Prop := repeat inversion_pointed_Prop_step. |