Library Common


Common helper definitions and facts for the project

@author Patryk Czarnik

Functions properties.

Section Functions.
  Variable A B: Set.
Inverse functions.
  Definition inverse (f: A → B) (g: B → A) :=
    ∀ a b, f a = b ↔ a = g b.

Bijetive function. Existence of such a function implies that A and B are isomorphic.
  Definition bijection (f: A → B) :=
    ∃ g: B → A, inverse f g.

  Definition flip3 {A B C: Set}
    (H: ∀ (a:A) (b:B) (c:C), Prop)
    (c:C) (a:A) (b:B) := H a b c.
End Functions.
Implicit Arguments inverse [A B].
Implicit Arguments bijection [A B].

Identity is an self-inverse function.
  Lemma inverse_id: ∀ A:Set, inverse (@id A) (@id A).
  Proof.
As the fact is trivial, the intuition tactic, with a little help from unfold, is smart enough to prove it.
    unfold inverse.
    intuition.
  Qed.

Identity is a bijection.
  Lemma bijection_id: ∀ A:Set, bijection (@id A).
  Proof.
We give id as the inverse function for id and refer to lemma inverse_id.
    unfold bijection.
    intro.
    ∃ (@id A).
    apply inverse_id.
  Qed.

Decidability of equality and other properties.

Section Dec.
  Variable P: Prop.

Property P is decidable in Prop.
  Definition propDec := P ∨ ¬P.

Property P is decidable in Set.
  Definition propDecS := {P}+{¬P}.

propDecS is stronger than propDec.
  Lemma PpropDecS_propDec: propDecS → propDec.
  Proof.
It derives from characteristic of inductive definitions over Set and Prop. When we destruct propDecS, the goal can be proven automatically (here using tauto).
    unfold propDec, propDecS.
    intros.
    destruct H; tauto.
  Qed.
End Dec.

Section EqDec.
  Variable A: Set.

Equality in A is decidable in Prop.
  Definition eqDec := ∀ a b:A, propDec (eq a b).

Equality in A is decidable in Set.
  Definition eqDecS := ∀ a b:A, propDecS (eq a b).

eqDecS is stronger than eqDec.
  Lemma PeqDecS_eqDec: eqDecS → eqDec.
  Proof.
We use lemma prop_decS_dec here.
    unfold eqDec, eqDecS.
    auto using PpropDecS_propDec.
  Qed.
End EqDec.

  Inductive TOneOrTwo (A: Set): Set :=
  | One (elem: A)
  | Two (elem1 elem2: A).
  Arguments TOneOrTwo A.
  Arguments One [A] elem.
  Arguments Two [A] elem1 elem2.

  Definition map_oneOrTwo (A B: Set) (f: A → B) (a12: TOneOrTwo A): TOneOrTwo B :=
    match a12 with
    | One a ⇒ One (f a)
    | Two a1 a2 ⇒ Two (f a1) (f a2)
    end.
  Arguments map_oneOrTwo [A B] f a12.

Section Lists.
  Require Import List.
  Require Import BoolEq.
  Variable K: Set.
  Variable A: Type.

  Hypothesis keyEqDec: eqDecS K.

  Inductive ListPrefix: list A → list A → Prop :=
  | ListPrefix_Nil: ∀ l, ListPrefix nil l
  | ListPrefix_Rec: ∀ p l x, ListPrefix p l → ListPrefix (x::p) (x::l).

  Lemma Pnth_error_length: ∀ (n: nat) (l: list A) (a: A),
    nth_error l n = value a → n < length l.
  Proof.
    intros n.
    induction n.
    intros.
    destruct l.
    simpl in ×.
    discriminate H.
    simpl.
    apply Lt.lt_0_Sn.

    intros.
    destruct l; simpl in ×.
    discriminate H.
    apply Lt.lt_n_S.
    eapply IHn.
    eassumption.
  Qed.

  Lemma Pnth_error_in: ∀ (n: nat) (l: list A) (a: A),
    nth_error l n = value a → In a l.
  Proof.
    intros n.
    induction n.
    intros.
    destruct l.
    simpl in ×.
    discriminate H.
    simpl in ×.
    injection H; intros.
    left.
    assumption.

    intros.
    destruct l; simpl in ×.
    discriminate H.
    right.
    apply IHn.
    assumption.
  Qed.

  Fixpoint findInListOfPairs (key: K) (l: list (K × A)) (default: A) {struct l}: A :=
  match l with
  | nil ⇒ default
  | ((k,a)::tl) ⇒
      if keyEqDec k key
        then a
        else findInListOfPairs key tl default
  end.
End Lists.
Implicit Arguments ListPrefix [A].
Implicit Arguments Pnth_error_length [A].
Implicit Arguments findInListOfPairs [K A].

Some additional tactics general enough to be put here.

Ltac f_equal_H H f :=
  match goal with
  | H: ?l = ?r |- _ ⇒
    assert (f l = f r);
    [f_equal; assumption | idtac]
  | _ ⇒ idtac
  end.

Ltac injection_clear H :=
  injection H; clear H; intro H.