SfLibSoftware Foundations Library
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 *)
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 : ∀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 : ∀b c,
andb b c = true → c = true.
Proof.
(* An exercise in Basics.v *)
Admitted.
Theorem beq_nat_sym : ∀(n m : nat),
beq_nat n m = beq_nat m n.
(* An exercise in Lists.v *)
Admitted.
Inductive ev : nat → Prop :=
| ev_0 : ev O
| ev_SS : ∀n:nat, ev n → ev (S (S n)).
Theorem andb_true : ∀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: ∀n n' : nat,
n ≠ n' →
beq_nat n n' = false.
Proof.
(* An exercise in Logic.v *)
Admitted.
Theorem ex_falso_quodlibet : ∀(P:Prop),
False → P.
Proof.
intros P contra.
inversion contra. Qed.
Theorem ev_not_ev_S : ∀n,
ev n → ¬ ev (S n).
Proof.
(* An exercise in Logic.v *)
Admitted.
Theorem ble_nat_true : ∀n m,
ble_nat n m = true → n ≤ m.
(* An exercise in Logic.v *)
Admitted.
Theorem ble_nat_false : ∀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 : ∀l, appears_in n (n::l)
| ai_later : ∀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 : ∀n m : nat, total_relation n m.
Inductive empty_relation : nat → nat → Prop := .
Definition relation (X:Type) := X → X → Prop.
Definition deterministic {X: Type} (R: relation X) :=
∀x y1 y2 : X, R x y1 → R x y2 → y1 = y2.
Inductive multi (X:Type) (R: relation X)
: X → X → Prop :=
| multi_refl : ∀(x : X),
multi X R x x
| multi_step : ∀(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 : ∀(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 :
∀(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 : ∀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 : ∀(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 : ∀(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} (Γ : partial_map A) (x:id) (T : A) :=
fun x' ⇒ if eq_id_dec x x' then Some T else Γ x'.
Lemma extend_eq : ∀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 : ∀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 : ∀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.
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.