1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
(** * 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_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.
Definition to_prop (x : pointed_Prop) : Prop
:= match x with
| trivial => True
| inject p => p
end.
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
| 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.
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
| [ H : inject _ = inject _ |- _ ] => progress (inversion H; clear H)
end.
Ltac inversion_pointed_Prop := repeat inversion_pointed_Prop_step.
|
