Add connectives about option pointed_Prop

1 files changed, 45 insertions, 0 deletions

diff --git a/src/Util/PointedProp.v b/src/Util/PointedProp.v
index 55cbe6d74..89bb578d6 100644
--- a/src/Util/PointedProp.v
+++ b/src/Util/PointedProp.v
@@ -5,6 +5,7 @@
 Require Import Crypto.Util.Notations.
 
 Delimit Scope pointed_prop_scope with pointed_prop.
+Delimit Scope option_pointed_prop_scope with option_pointed_prop.
 Inductive pointed_Prop := trivial | inject (_ : Prop).
 Bind Scope pointed_prop_scope with pointed_Prop.
 
@@ -16,6 +17,14 @@ Definition to_prop (x : pointed_Prop) : Prop
 
 Coercion option_pointed_Prop_of_bool (x : bool) : option pointed_Prop
   := if x then Some trivial else None.
+Coercion option_pointed_Prop_of_pointed_Prop (x : pointed_Prop) : option pointed_Prop
+  := Some x.
+
+Definition prop_of_option (x : option pointed_Prop) : Prop
+  := match x with
+     | Some p => to_prop p
+     | None => False
+     end.
 
 Definition and_pointed_Prop (x y : pointed_Prop) : pointed_Prop
   := match x, y with
@@ -38,9 +47,45 @@ Definition impl_pointed_Prop (x y : pointed_Prop) : pointed_Prop
      | inject p, inject q => inject (p -> q)
      end.
 
+Definition not_option_pointed_Prop (x : option pointed_Prop) : option pointed_Prop
+  := match x with
+     | Some trivial => None
+     | None => Some trivial
+     | Some (inject p) => Some (inject (~p))
+     end.
+Arguments not_option_pointed_Prop _%option_pointed_prop.
+
+Definition and_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
+  := match x, y with
+     | Some x, Some y => Some (and_pointed_Prop x y)
+     | _, _ => None
+     end.
+Arguments and_option_pointed_Prop (_ _)%option_pointed_prop.
+
+Definition or_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
+  := match x, y with
+     | Some x, Some y => Some (or_pointed_Prop x y)
+     | Some x, None => Some x
+     | None, Some y => Some y
+     | None, None => None
+     end.
+Arguments or_option_pointed_Prop (_ _)%option_pointed_prop.
+
+Definition impl_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
+  := match x, y with
+     | None, _ => Some trivial
+     | Some x, Some y => Some (impl_pointed_Prop x y)
+     | Some p, None => not_option_pointed_Prop p
+     end.
+Arguments impl_option_pointed_Prop (_ _)%option_pointed_prop.
+
 Infix "/\" := and_pointed_Prop : pointed_prop_scope.
 Infix "\/" := or_pointed_Prop : pointed_prop_scope.
 Infix "->" := impl_pointed_Prop : pointed_prop_scope.
+Infix "/\" := and_option_pointed_Prop : option_pointed_prop_scope.
+Infix "\/" := or_option_pointed_Prop : option_pointed_prop_scope.
+Infix "->" := impl_option_pointed_Prop : option_pointed_prop_scope.
+Notation "~ P" := (not_option_pointed_Prop P) : option_pointed_prop_scope.
 
 Ltac inversion_pointed_Prop_step :=
   match goal with