Permalink
Fetching contributors…
Cannot retrieve contributors at this time
252 lines (199 sloc) 6.65 KB
(** * SfLib: Software Foundations Library *)
(** Here we collect together several useful definitions and theorems
from Basics.v, List.v, Poly.v, Ind.v, and Logic.v that are not
already in the Coq standard library. From now on we can [Import]
or [Export] this file, instead of cluttering our environment with
all the examples and false starts in those files. *)
(** * From the Coq Standard Library *)
Require Omega. (* needed for using the [omega] tactic *)
Require Export Bool.
Require Export List.
Export ListNotations.
Require Export Arith.
Require Export Arith.EqNat. (* Contains [beq_nat], among other things *)
(** * From Basics.v *)
Definition admit {T: Type} : T. Admitted.
Require String. Open Scope string_scope.
Ltac move_to_top x :=
match reverse goal with
| H : _ |- _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case" ].
Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.
Fixpoint ble_nat (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => ble_nat n' m'
end
end.
Theorem andb_true_elim1 : forall b c,
andb b c = true -> b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
reflexivity.
Case "b = false".
rewrite <- H. reflexivity. Qed.
Theorem andb_true_elim2 : forall b c,
andb b c = true -> c = true.
Proof.
(* An exercise in Basics.v *)
Admitted.
Theorem beq_nat_sym : forall (n m : nat),
beq_nat n m = beq_nat m n.
(* An exercise in Lists.v *)
Admitted.
(** * From Props.v *)
Inductive ev : nat -> Prop :=
| ev_0 : ev O
| ev_SS : forall n:nat, ev n -> ev (S (S n)).
(** * From Logic.v *)
Theorem andb_true : forall b c,
andb b c = true -> b = true /\ c = true.
Proof.
intros b c H.
destruct b.
destruct c.
apply conj. reflexivity. reflexivity.
inversion H.
inversion H. Qed.
Theorem false_beq_nat: forall n n' : nat,
n <> n' ->
beq_nat n n' = false.
Proof.
(* An exercise in Logic.v *)
Admitted.
Theorem ex_falso_quodlibet : forall (P:Prop),
False -> P.
Proof.
intros P contra.
inversion contra. Qed.
Theorem ev_not_ev_S : forall n,
ev n -> ~ ev (S n).
Proof.
(* An exercise in Logic.v *)
Admitted.
Theorem ble_nat_true : forall n m,
ble_nat n m = true -> n <= m.
(* An exercise in Logic.v *)
Admitted.
Theorem ble_nat_false : forall n m,
ble_nat n m = false -> ~(n <= m).
(* An exercise in Logic.v *)
Admitted.
Inductive appears_in (n : nat) : list nat -> Prop :=
| ai_here : forall l, appears_in n (n::l)
| ai_later : forall m l, appears_in n l -> appears_in n (m::l).
Inductive next_nat (n:nat) : nat -> Prop :=
| nn : next_nat n (S n).
Inductive total_relation : nat -> nat -> Prop :=
tot : forall n m : nat, total_relation n m.
Inductive empty_relation : nat -> nat -> Prop := .
(** * From Later Files *)
Definition relation (X:Type) := X -> X -> Prop.
Definition deterministic {X: Type} (R: relation X) :=
forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
Inductive multi (X:Type) (R: relation X)
: X -> X -> Prop :=
| multi_refl : forall (x : X),
multi X R x x
| multi_step : forall (x y z : X),
R x y ->
multi X R y z ->
multi X R x z.
Implicit Arguments multi [[X]].
Tactic Notation "multi_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "multi_refl" | Case_aux c "multi_step" ].
Theorem multi_R : forall (X:Type) (R:relation X) (x y : X),
R x y -> multi R x y.
Proof.
intros X R x y r.
apply multi_step with y. apply r. apply multi_refl. Qed.
Theorem multi_trans :
forall (X:Type) (R: relation X) (x y z : X),
multi R x y ->
multi R y z ->
multi R x z.
Proof.
(* FILL IN HERE *) Admitted.
(** Identifiers and polymorphic partial maps. *)
Inductive id : Type :=
Id : nat -> id.
Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
Proof.
intros id1 id2.
destruct id1 as [n1]. destruct id2 as [n2].
destruct (eq_nat_dec n1 n2) as [Heq | Hneq].
Case "n1 = n2".
left. rewrite Heq. reflexivity.
Case "n1 <> n2".
right. intros contra. inversion contra. apply Hneq. apply H0.
Defined.
Lemma eq_id : forall (T:Type) x (p q:T),
(if eq_id_dec x x then p else q) = p.
Proof.
intros.
destruct (eq_id_dec x x); try reflexivity.
apply ex_falso_quodlibet; auto.
Qed.
Lemma neq_id : forall (T:Type) x y (p q:T), x <> y ->
(if eq_id_dec x y then p else q) = q.
Proof.
(* FILL IN HERE *) Admitted.
Definition partial_map (A:Type) := id -> option A.
Definition empty {A:Type} : partial_map A := (fun _ => None).
Notation "'\empty'" := empty.
Definition extend {A:Type} (Gamma : partial_map A) (x:id) (T : A) :=
fun x' => if eq_id_dec x x' then Some T else Gamma x'.
Lemma extend_eq : forall A (ctxt: partial_map A) x T,
(extend ctxt x T) x = Some T.
Proof.
intros. unfold extend. rewrite eq_id; auto.
Qed.
Lemma extend_neq : forall A (ctxt: partial_map A) x1 T x2,
x2 <> x1 ->
(extend ctxt x2 T) x1 = ctxt x1.
Proof.
intros. unfold extend. rewrite neq_id; auto.
Qed.
Lemma extend_shadow : forall A (ctxt: partial_map A) t1 t2 x1 x2,
extend (extend ctxt x2 t1) x2 t2 x1 = extend ctxt x2 t2 x1.
Proof with auto.
intros. unfold extend. destruct (eq_id_dec x2 x1)...
Qed.
(** -------------------- *)
(** * Some useful tactics *)
Tactic Notation "solve_by_inversion_step" tactic(t) :=
match goal with
| H : _ |- _ => solve [ inversion H; subst; t ]
end
|| fail "because the goal is not solvable by inversion.".
Tactic Notation "solve" "by" "inversion" "1" :=
solve_by_inversion_step idtac.
Tactic Notation "solve" "by" "inversion" "2" :=
solve_by_inversion_step (solve by inversion 1).
Tactic Notation "solve" "by" "inversion" "3" :=
solve_by_inversion_step (solve by inversion 2).
Tactic Notation "solve" "by" "inversion" :=
solve by inversion 1.
(** $Date: 2014-12-31 12:04:02 -0500 (Wed, 31 Dec 2014) $ *)