Permalink
Fetching contributors…
Cannot retrieve contributors at this time
267 lines (217 sloc) 7.05 KB
(** * SfLib: Software Foundations Library *)
(* $Date: 2013-01-16 22:29:57 -0500 (Wed, 16 Jan 2013) $ *)
(** 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.
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.
(* From Poly.v *)
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
(at level 60, right associativity).
(** * 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 ex_falso_quodlibet : forall (P:Prop),
False -> P.
Proof.
intros P contra.
inversion contra. Qed.
Theorem O_le_n : forall n,
0 <= n.
Proof.
induction n as [| n'].
Case "n = 0". apply le_n.
Case "n = S n'". apply le_S. apply IHn'.
Qed.
Theorem n_le_m__Sn_le_Sm : forall n m,
n <= m -> S n <= S m.
Proof.
intros. induction H as [| m'].
Case "H = n <= n". apply le_n.
Case "H = n <= S m'". apply le_S in IHle. apply IHle.
Qed.
Theorem ble_nat_true : forall n m,
ble_nat n m = true -> n <= m.
Proof.
intros. generalize dependent m.
induction n as [| n'];
intros.
Case "n = 0". apply O_le_n.
Case "n = S n'". destruct m. inversion H.
simpl in H. apply n_le_m__Sn_le_Sm. apply IHn'. apply H.
Qed.
Lemma ble_nat_true_iff : forall n m : nat,
ble_nat n m = true <-> n <= m.
Proof.
intros n m. split. apply ble_nat_true.
generalize dependent m. induction n; intros m H. reflexivity.
simpl. destruct m. inversion H.
apply le_S_n in H. apply IHn. assumption.
Qed.
Theorem false_beq_nat : forall n m : nat,
n <> m ->
beq_nat n m = false.
Proof.
intros. generalize dependent m.
induction n;
intros;
unfold not in H;
destruct m;
simpl.
destruct H. reflexivity.
reflexivity.
reflexivity.
apply IHn. unfold not.
intros H'. apply H.
rewrite H'. reflexivity.
Qed.
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.
(* Identifiers and polymorphic partial maps. *)
Inductive id : Type :=
Id : nat -> id.
Definition beq_id id1 id2 :=
match (id1, id2) with
(Id n1, Id n2) => beq_nat n1 n2
end.
Theorem beq_id_refl : forall i,
true = beq_id i i.
Proof.
intros. destruct i.
apply beq_nat_refl. Qed.
Theorem beq_id_eq : forall i1 i2,
true = beq_id i1 i2 -> i1 = i2.
Proof.
intros i1 i2 H.
destruct i1. destruct i2.
apply beq_nat_eq in H. subst.
reflexivity. Qed.
Theorem beq_id_false_not_eq : forall i1 i2,
beq_id i1 i2 = false -> i1 <> i2.
Proof.
intros i1 i2 H.
destruct i1. destruct i2.
apply beq_nat_false in H.
intros C. apply H. inversion C. reflexivity. Qed.
Definition partial_map (A:Type) := id -> option A.
Definition empty {A:Type} : partial_map A := (fun _ => None).
Definition extend {A:Type} (Gamma : partial_map A) (x:id) (T : A) :=
fun x' => if beq_id 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 <- beq_id_refl. auto.
Qed.
Lemma extend_neq : forall A (ctxt: partial_map A) x1 T x2,
beq_id x2 x1 = false ->
(extend ctxt x2 T) x1 = ctxt x1.
Proof.
intros. unfold extend. rewrite H. 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 (beq_id 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.