From 21fe0146350bad3a4ff555dd0c9d17f82508bbee Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 12:56:44 -0700 Subject: Add connectives about option pointed_Prop --- src/Util/PointedProp.v | 45 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) (limited to 'src/Util/PointedProp.v') 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 -- cgit v1.2.3