coqrel/BoolRel.v at master · CertiKOS/coqrel · GitHub

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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
Require Import LogicalRelations.
Require Export Coq.Bool.Bool.


(** * Relations for [sumbool] *)

(** ** Symmetric relation *)

(** NB: With proof irrelevance this is the same as [eq]. *)

Inductive sumbool_rel {P1 P2 Q1 Q2}: rel (sumbool P1 Q1) (sumbool P2 Q2):=
  | left_rel_def H1 H2: sumbool_rel (left H1) (left H2)
  | right_rel_def H1 H2: sumbool_rel (right H1) (right H2).

Global Instance left_rel:
  Monotonic (@left) (forallr _ _ : ⊤, forallr _ _ : ⊤, ⊤ ++> sumbool_rel).
Proof.
  constructor; eauto.
Qed.

Global Instance right_rel:
  Monotonic (@right) (forallr _ _ : ⊤, forallr _ _ : ⊤, ⊤ ++> sumbool_rel).
Proof.
  constructor; eauto.
Qed.

(** ** Directed relation *)

Inductive sumbool_le {P1 P2 Q1 Q2}: rel (sumbool P1 Q1) (sumbool P2 Q2):=
  | left_le b1 H2: Related b1 (left H2) sumbool_le
  | right_le H1 b2: Related (right H1) b2 sumbool_le.

Global Existing Instance left_le.
Global Existing Instance right_le.


(** * Definitions for [Bool.le] *)

(** ** Properties *)

Global Instance leb_preo:
  PreOrder Bool.le.
Proof.
  split.
  - intros [|]; simpl; eauto.
  - intros [|]; simpl; eauto.
    intros [|]; simpl; eauto.
    discriminate.
Qed.

Lemma leb_rdestruct:
  RDestruct Bool.le (fun P => P false false /\ P true true /\ P false true).
Proof.
  intros b1 b2 Hb P (HPff & HPtt & HPft).
  destruct b1, b2; eauto; discriminate.
Qed.

Global Hint Extern 0 (RDestruct Bool.le _) =>
  eapply leb_rdestruct : typeclass_instances.

Global Instance leb_transport_eq_true x y:
  Transport Bool.le x y (x = true) (y = true).
Proof.
  clear.
  destruct x, y; firstorder.
Qed.

(** ** Monotonicity of various definitions *)

Lemma true_leb b:
  Related b true Bool.le.
Proof.
  destruct b; reflexivity.
Qed.

Global Hint Extern 0 (Related _ true _) =>
  eapply true_leb : typeclass_instances.

Lemma false_leb b:
  Related false b Bool.le.
Proof.
  destruct b; reflexivity.
Qed.

Global Hint Extern 0 (Related false _ _) =>
  eapply false_leb : typeclass_instances.

Global Instance negb_leb:
  Monotonic negb (Bool.le --> Bool.le).
Proof.
  unfold negb.
  rauto.
Qed.

Global Instance andb_leb:
  Monotonic andb (Bool.le ++> Bool.le ++> Bool.le).
Proof.
  unfold andb.
  rauto.
Qed.

Global Instance orb_leb:
  Monotonic orb (Bool.le ++> Bool.le ++> Bool.le).
Proof.
  unfold orb.
  rauto.
Qed.

Global Instance implb_leb:
  Monotonic implb (Bool.le --> Bool.le ++> Bool.le).
Proof.
  unfold implb.
  rauto.
Qed.