SfLibSoftware Foundations Library

(* $Date: 2011-03-14 20:08:53 -0400 (Mon, 14 Mar 2011) $ *)

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

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'

Theorem andb_true_elim1 : b c,
  andb b c = true b = true.
  intros b c H.
  destruct b.
  Case "b = true".
  Case "b = false".
    rewrite H. reflexivity. Qed.

Theorem andb_true_elim2 : b c,
  andb b c = true c = true.
(* An exercise in Basics.v *)

Theorem beq_nat_sym : (n m : nat),
  beq_nat n m = beq_nat m n.
(* An exercise in Lists.v *)

(* 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 : n:nat, ev n ev (S (S n)).

From Logic.v

Theorem andb_true : b c,
  andb b c = true b = true c = true.
  intros b c H.
  destruct b.
    destruct c.
      apply conj. reflexivity. reflexivity.
      inversion H.
    inversion H. Qed.

Theorem not_eq_beq_false : n n' : nat,
     n <> n'
     beq_nat n n' = false.
(* An exercise in Logic.v *)

Theorem ex_falso_quodlibet : (P:Prop),
  False P.
  intros P contra.
  inversion contra. Qed.

Theorem ev_not_ev_S : n,
  ev n ~ ev (S n).
(* An exercise in Logic.v *)

Theorem ble_nat_true : n m,
  ble_nat n m = true n <= m.
(* An exercise in Logic.v *)

Theorem ble_nat_false : n m,
  ble_nat n m = false ~(n <= m).
(* An exercise in Logic.v *)

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).

Definition relation (X:Type) := X X Prop.

Definition partial_function {X: Type} (R: relation X) :=
   x y1 y2 : X, R x y1 R x y2 y1 = y2.

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 := .

Inductive refl_step_closure (X:Type) (R: relation X)
                            : X X Prop :=
  | rsc_refl : (x : X),
                 refl_step_closure X R x x
  | rsc_step : (x y z : X),
                    R x y
                    refl_step_closure X R y z
                    refl_step_closure X R x z.
Implicit Arguments refl_step_closure [[X]].

Tactic Notation "rsc_cases" tactic(first) ident(c) :=
  [ Case_aux c "rsc_refl" | Case_aux c "rsc_step" ].

Theorem rsc_R : (X:Type) (R:relation X) (x y : X),
       R x y refl_step_closure R x y.
  intros X R x y r.
  apply rsc_step with y. apply r. apply rsc_refl. Qed.

Theorem rsc_trans :
   (X:Type) (R: relation X) (x y z : X),
      refl_step_closure R x y
      refl_step_closure R y z
      refl_step_closure R x z.
  (* FILL IN HERE *) Admitted.

(* 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

Theorem beq_id_refl : i,
  true = beq_id i i.
  intros. destruct i.
  apply beq_nat_refl. Qed.

Theorem beq_id_eq : i1 i2,
  true = beq_id i1 i2 i1 = i2.
  intros i1 i2 H.
  destruct i1. destruct i2.
  apply beq_nat_eq in H. subst.
  reflexivity. Qed.

Theorem beq_id_false_not_eq : i1 i2,
  beq_id i1 i2 = false i1 <> i2.
  intros i1 i2 H.
  destruct i1. destruct i2.
  apply beq_nat_false in H.
  intros C. apply H. inversion C. reflexivity. Qed.

Theorem not_eq_beq_id_false : i1 i2,
  i1 <> i2 beq_id i1 i2 = false.
  intros i1 i2 H.
  destruct i1. destruct i2.
  assert (n <> n0).
    intros C. subst. apply H. reflexivity.
  apply not_eq_beq_false. assumption. Qed.

Theorem beq_id_sym: i1 i2,
  beq_id i1 i2 = beq_id i2 i1.
  intros i1 i2. destruct i1. destruct i2. apply beq_nat_sym. Qed.

Definition partial_map (A:Type) := id option A.

Definition empty {A:Type} : partial_map A := (fun _ => None).

Definition extend {A:Type} (Γ : partial_map A) (x:id) (T : A) :=
  fun x' => if beq_id x x' then Some T else Γ x'.

Lemma extend_eq : A (ctxt: partial_map A) x T,
  (extend ctxt x T) x = Some T.
  intros. unfold extend. rewrite beq_id_refl. auto.

Lemma extend_neq : A (ctxt: partial_map A) x1 T x2,
  beq_id x2 x1 = false
  (extend ctxt x2 T) x1 = ctxt x1.
  intros. unfold extend. rewrite H. auto.

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 (beq_id x2 x1)...

Some useful tactics

Tactic Notation "solve_by_inversion_step" tactic(t) :=
  match goal with
  | H : _ _ => solve [ inversion H; subst; t ]
   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.