From ed88b28433ef90f8be554803a4fe852a6634ee87 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 11:54:43 -0700 Subject: Add a file about pointed Props --- src/Util/PointedProp.v | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 src/Util/PointedProp.v (limited to 'src/Util/PointedProp.v') 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. -- cgit v1.2.3