Skip to content

Commit db8e43e

Browse files
TiarkRompfTiarkRompf
committed
add SfLib.v
1 parent 2ed591e commit db8e43e

File tree

1 file changed

+251
-0
lines changed

1 file changed

+251
-0
lines changed

‎dev2015/SfLib.v

Lines changed: 251 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,251 @@
1+
(** * SfLib: Software Foundations Library *)
2+
3+
(** Here we collect together several useful definitions and theorems
4+
from Basics.v, List.v, Poly.v, Ind.v, and Logic.v that are not
5+
already in the Coq standard library. From now on we can [Import]
6+
or [Export] this file, instead of cluttering our environment with
7+
all the examples and false starts in those files. *)
8+
9+
(** * From the Coq Standard Library *)
10+
11+
Require Omega. (* needed for using the [omega] tactic *)
12+
Require Export Bool.
13+
Require Export List.
14+
Export ListNotations.
15+
Require Export Arith.
16+
Require Export Arith.EqNat. (* Contains [beq_nat], among other things *)
17+
18+
(** * From Basics.v *)
19+
20+
Definition admit {T: Type} : T. Admitted.
21+
22+
Require String. Open Scope string_scope.
23+
24+
Ltac move_to_top x :=
25+
match reverse goal with
26+
| H : _ |- _ => try move x after H
27+
end.
28+
29+
Tactic Notation "assert_eq" ident(x) constr(v) :=
30+
let H := fresh in
31+
assert (x = v) as H by reflexivity;
32+
clear H.
33+
34+
Tactic Notation "Case_aux" ident(x) constr(name) :=
35+
first [
36+
set (x := name); move_to_top x
37+
| assert_eq x name; move_to_top x
38+
| fail 1 "because we are working on a different case" ].
39+
40+
Tactic Notation "Case" constr(name) := Case_aux Case name.
41+
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
42+
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
43+
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
44+
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
45+
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
46+
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
47+
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.
48+
49+
Fixpoint ble_nat (n m : nat) : bool :=
50+
match n with
51+
| O => true
52+
| S n' =>
53+
match m with
54+
| O => false
55+
| S m' => ble_nat n' m'
56+
end
57+
end.
58+
59+
Theorem andb_true_elim1 : forall b c,
60+
andb b c = true -> b = true.
61+
Proof.
62+
intros b c H.
63+
destruct b.
64+
Case "b = true".
65+
reflexivity.
66+
Case "b = false".
67+
rewrite <- H. reflexivity. Qed.
68+
69+
Theorem andb_true_elim2 : forall b c,
70+
andb b c = true -> c = true.
71+
Proof.
72+
(* An exercise in Basics.v *)
73+
Admitted.
74+
75+
Theorem beq_nat_sym : forall (n m : nat),
76+
beq_nat n m = beq_nat m n.
77+
(* An exercise in Lists.v *)
78+
Admitted.
79+
80+
(** * From Props.v *)
81+
82+
Inductive ev : nat -> Prop :=
83+
| ev_0 : ev O
84+
| ev_SS : forall n:nat, ev n -> ev (S (S n)).
85+
86+
(** * From Logic.v *)
87+
88+
Theorem andb_true : forall b c,
89+
andb b c = true -> b = true /\ c = true.
90+
Proof.
91+
intros b c H.
92+
destruct b.
93+
destruct c.
94+
apply conj. reflexivity. reflexivity.
95+
inversion H.
96+
inversion H. Qed.
97+
98+
Theorem false_beq_nat: forall n n' : nat,
99+
n <> n' ->
100+
beq_nat n n' = false.
101+
Proof.
102+
(* An exercise in Logic.v *)
103+
Admitted.
104+
105+
Theorem ex_falso_quodlibet : forall (P:Prop),
106+
False -> P.
107+
Proof.
108+
intros P contra.
109+
inversion contra. Qed.
110+
111+
Theorem ev_not_ev_S : forall n,
112+
ev n -> ~ ev (S n).
113+
Proof.
114+
(* An exercise in Logic.v *)
115+
Admitted.
116+
117+
Theorem ble_nat_true : forall n m,
118+
ble_nat n m = true -> n <= m.
119+
(* An exercise in Logic.v *)
120+
Admitted.
121+
122+
Theorem ble_nat_false : forall n m,
123+
ble_nat n m = false -> ~(n <= m).
124+
(* An exercise in Logic.v *)
125+
Admitted.
126+
127+
Inductive appears_in (n : nat) : list nat -> Prop :=
128+
| ai_here : forall l, appears_in n (n::l)
129+
| ai_later : forall m l, appears_in n l -> appears_in n (m::l).
130+
131+
Inductive next_nat (n:nat) : nat -> Prop :=
132+
| nn : next_nat n (S n).
133+
134+
Inductive total_relation : nat -> nat -> Prop :=
135+
tot : forall n m : nat, total_relation n m.
136+
137+
Inductive empty_relation : nat -> nat -> Prop := .
138+
139+
(** * From Later Files *)
140+
141+
Definition relation (X:Type) := X -> X -> Prop.
142+
143+
Definition deterministic {X: Type} (R: relation X) :=
144+
forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
145+
146+
Inductive multi (X:Type) (R: relation X)
147+
: X -> X -> Prop :=
148+
| multi_refl : forall (x : X),
149+
multi X R x x
150+
| multi_step : forall (x y z : X),
151+
R x y ->
152+
multi X R y z ->
153+
multi X R x z.
154+
Implicit Arguments multi [[X]].
155+
156+
Tactic Notation "multi_cases" tactic(first) ident(c) :=
157+
first;
158+
[ Case_aux c "multi_refl" | Case_aux c "multi_step" ].
159+
160+
Theorem multi_R : forall (X:Type) (R:relation X) (x y : X),
161+
R x y -> multi R x y.
162+
Proof.
163+
intros X R x y r.
164+
apply multi_step with y. apply r. apply multi_refl. Qed.
165+
166+
Theorem multi_trans :
167+
forall (X:Type) (R: relation X) (x y z : X),
168+
multi R x y ->
169+
multi R y z ->
170+
multi R x z.
171+
Proof.
172+
(* FILL IN HERE *) Admitted.
173+
174+
(** Identifiers and polymorphic partial maps. *)
175+
176+
Inductive id : Type :=
177+
Id : nat -> id.
178+
179+
Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
180+
Proof.
181+
intros id1 id2.
182+
destruct id1 as [n1]. destruct id2 as [n2].
183+
destruct (eq_nat_dec n1 n2) as [Heq | Hneq].
184+
Case "n1 = n2".
185+
left. rewrite Heq. reflexivity.
186+
Case "n1 <> n2".
187+
right. intros contra. inversion contra. apply Hneq. apply H0.
188+
Defined.
189+
190+
Lemma eq_id : forall (T:Type) x (p q:T),
191+
(if eq_id_dec x x then p else q) = p.
192+
Proof.
193+
intros.
194+
destruct (eq_id_dec x x); try reflexivity.
195+
apply ex_falso_quodlibet; auto.
196+
Qed.
197+
198+
Lemma neq_id : forall (T:Type) x y (p q:T), x <> y ->
199+
(if eq_id_dec x y then p else q) = q.
200+
Proof.
201+
(* FILL IN HERE *) Admitted.
202+
203+
Definition partial_map (A:Type) := id -> option A.
204+
205+
Definition empty {A:Type} : partial_map A := (fun _ => None).
206+
207+
Notation "'\empty'" := empty.
208+
209+
Definition extend {A:Type} (Gamma : partial_map A) (x:id) (T : A) :=
210+
fun x' => if eq_id_dec x x' then Some T else Gamma x'.
211+
212+
Lemma extend_eq : forall A (ctxt: partial_map A) x T,
213+
(extend ctxt x T) x = Some T.
214+
Proof.
215+
intros. unfold extend. rewrite eq_id; auto.
216+
Qed.
217+
218+
Lemma extend_neq : forall A (ctxt: partial_map A) x1 T x2,
219+
x2 <> x1 ->
220+
(extend ctxt x2 T) x1 = ctxt x1.
221+
Proof.
222+
intros. unfold extend. rewrite neq_id; auto.
223+
Qed.
224+
225+
Lemma extend_shadow : forall A (ctxt: partial_map A) t1 t2 x1 x2,
226+
extend (extend ctxt x2 t1) x2 t2 x1 = extend ctxt x2 t2 x1.
227+
Proof with auto.
228+
intros. unfold extend. destruct (eq_id_dec x2 x1)...
229+
Qed.
230+
231+
(** -------------------- *)
232+
233+
(** * Some useful tactics *)
234+
235+
Tactic Notation "solve_by_inversion_step" tactic(t) :=
236+
match goal with
237+
| H : _ |- _ => solve [ inversion H; subst; t ]
238+
end
239+
|| fail "because the goal is not solvable by inversion.".
240+
241+
Tactic Notation "solve" "by" "inversion" "1" :=
242+
solve_by_inversion_step idtac.
243+
Tactic Notation "solve" "by" "inversion" "2" :=
244+
solve_by_inversion_step (solve by inversion 1).
245+
Tactic Notation "solve" "by" "inversion" "3" :=
246+
solve_by_inversion_step (solve by inversion 2).
247+
Tactic Notation "solve" "by" "inversion" :=
248+
solve by inversion 1.
249+
250+
(** $Date: 2014-12-31 12:04:02 -0500 (Wed, 31 Dec 2014) $ *)
251+

0 commit comments

Comments
 (0)