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: AB) (g: BA) :=
     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: AB) :=
     g: BA, 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).
As the fact is trivial, the intuition tactic, with a little help from unfold, is smart enough to prove it.
    unfold inverse.

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

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: propDecSpropDec.
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.
    destruct H; tauto.
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: eqDecSeqDec.
We use lemma prop_decS_dec here.
    unfold eqDec, eqDecS.
    auto using PpropDecS_propDec.
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: AB) (a12: TOneOrTwo A): TOneOrTwo B :=
    match a12 with
    | One aOne (f a)
    | Two a1 a2Two (f a1) (f a2)
  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 Alist AProp :=
  | ListPrefix_Nil: l, ListPrefix nil l
  | ListPrefix_Rec: p l x, ListPrefix p lListPrefix (x::p) (x::l).

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

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

  Lemma Pnth_error_in: (n: nat) (l: list A) (a: A),
    nth_error l n = value aIn a l.
    intros n.
    induction n.
    destruct l.
    simpl in ×.
    discriminate H.
    simpl in ×.
    injection H; intros.

    destruct l; simpl in ×.
    discriminate H.
    apply IHn.

  Fixpoint findInListOfPairs (key: K) (l: list (K × A)) (default: A) {struct l}: A :=
  match l with
  | nildefault
  | ((k,a)::tl) ⇒
      if keyEqDec k key
        then a
        else findInListOfPairs key tl default
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

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