This file contains definitions and proofs from the Base Library for the ICL lecture.
  • Version: 3 October 2016
  • Author: Gert Smolka, Saarland University
  • Acknowlegments: Sigurd Schneider, Dominik Kirst, Yannick Forster

Require Export Bool Omega List Setoid Morphisms Tactics.

Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Records.
Global Unset Printing Implicit Defensive.
Global Set Regular Subst Tactic.


Export ListNotations.
Notation "x 'el' A" := (In x A) (at level 70).
Notation "A <<= B" := (incl A B) (at level 70).
Notation "| A |" := (length A) (at level 65).

Hint Extern 4 =>
match goal with
|[ H: ?x el nil |- _ ] => destruct H

Lemma in_sing {X} (x y:X) :
    x el [y] -> x = y.
    cbn. intros [[]|[]]. reflexivity.

Lemma in_concat_iff A l (a:A) : a el concat l <-> exists l', a el l' /\ l' el l.
  induction l; cbn.
  - intuition. now destruct H.
  - rewrite in_app_iff, IHl. firstorder subst. auto.

Lemma incl_nil X (A : list X) :
  nil <<= A.
Proof. intros x []. Qed.

Hint Rewrite <- app_assoc : list.
Hint Rewrite rev_app_distr map_app prod_length : list.
Hint Resolve in_eq in_nil in_cons in_or_app.
Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app incl_nil.


Definition dec (X: Prop) : Type := {X} + {~ X}.
Coercion dec2bool P (d: dec P) := if d then true else false.
Existing Class dec.
Definition Dec (X: Prop) (d: dec X) : dec X := d.
Arguments Dec X {d}.

Hint Extern 4 => (* Improves type class inference *)
match goal with
  | [ |- dec ((fun _ => _) _) ] => cbn
end : typeclass_instances.

Tactic Notation "decide" constr(p) :=
  destruct (Dec p).
Tactic Notation "decide" constr(p) "as" simple_intropattern(i) :=
  destruct (Dec p) as i.
Tactic Notation "decide" "_" :=
  destruct (Dec _).

Discrete types

Notation "'eq_dec' X" := (forall x y : X, dec (x=y)) (at level 70).

Structure eqType := EqType {
  eqType_X :> Type;
  eqType_dec : eq_dec eqType_X }.

Arguments EqType X {_} : rename.
Canonical Structure eqType_CS X (A: eq_dec X) := EqType X.
Existing Instance eqType_dec.

Instance list_eq_dec X :
  eq_dec X -> eq_dec (list X).
  unfold dec. decide equality.


Ltac inv H := inversion H; subst; try clear H.

Tactic Notation "destruct" "_":=
  match goal with
  | [ |- context[match ?X with _ => _ end] ] => destruct X
  | [ H : context[match ?X with _ => _ end] |- _ ] => destruct X

Tactic Notation "destruct" "_" "eqn" ":" ident(E) :=
  match goal with
  | [ |- context[match ?X with _ => _ end] ] => destruct X eqn:E
  | [ H : context[match ?X with _ => _ end] |- _ ] => destruct X eqn:E

Tactic Notation "destruct" "*" :=
  repeat destruct _.

Tactic Notation "destruct" "*" "eqn" ":" ident(E) :=
  repeat (let E := fresh E in destruct _ eqn:E; try progress inv E); try now congruence.

Tactic Notation "destruct" "*" "eqn" ":" "_" := destruct * eqn:E.

Hint Extern 4 =>
match goal with
|[ H: False |- _ ] => destruct H
|[ H: true=false |- _ ] => discriminate H
|[ H: false=true |- _ ] => discriminate H

Size Induction
Lemma size_induction X (f : X -> nat) (p : X -> Prop) :
  (forall x, (forall y, f y < f x -> p y) -> p x) ->
  forall x, p x.

  intros IH x. apply IH.
  assert (G: forall n y, f y < n -> p y).
  { intros n. induction n.
    - intros y B. exfalso. omega.
    - intros y B. apply IH. intros z C. apply IHn. omega. }
  apply G.

Finite Types

The definitions of finite types are adopted from the Bachelor Thesis of Jan Menz.
This function counts the number of occurences of an element in a given list and returns the result
Fixpoint count (X: Type) `{eq_dec X} (A: list X) (x: X) {struct A} : nat :=
  match A with
  | nil => O
  | cons y A' => if Dec (x=y) then S(count A' x) else count A' x end.

Class finTypeC (type:eqType) : Type := FinTypeC {
                                            enum: list type;
                                            enum_ok: forall x: type, count enum x = 1

Structure finType : Type := FinType {
                                type:> eqType;
                                class: finTypeC type }.

Arguments FinType type {class}.
Existing Instance class | 0.

Canonical Structure finType_CS (X : Type) {p : eq_dec X} {class : finTypeC (EqType X)} : finType := FinType (EqType X).

Definition elem (F: finType) := @enum (type F) (class F).
Hint Unfold elem.
Hint Unfold class.

dec is used to destruct all decisions appearing in the goal or assumptions.
Ltac dec := repeat (destruct Dec).

Lemma countIn (X:eqType) (x:X) A:
  count A x > 0 -> x el A.
  induction A.
  - cbn. omega.
  - cbn. dec.
    + intros. left. symmetry. exact e.
    + intros. right. apply IHA. exact H.

Lemma elem_spec (X: finType) (x:X) : x el (elem X).
  apply countIn. pose proof (enum_ok x) as H. unfold elem. omega.

Hint Resolve elem_spec.
Hint Resolve enum_ok.

If a list is split somewhere in two list the number of occurences of an element in the list is equal to the sum of the number of occurences in the left and the right part.
Lemma countSplit (X: eqType) (A B: list X) (x: X) : count A x + count B x = count (A ++ B) x.
  induction A.
  - reflexivity.
  - cbn. decide (x=a).
    +cbn. f_equal; exact IHA.
    + exact IHA.

Lemma notInZero (X: eqType) (x: X) A :
  not (x el A) <-> count A x = 0.
  split; induction A.
  - reflexivity.
  - intros H. cbn in *. dec.
    + exfalso. apply H. left. congruence.
    + apply IHA. intros F. apply H. now right.
  - tauto.
  - cbn. dec.
    + subst a. omega.
    + intros H [E | E].
      * now symmetry in E.
      * tauto.

Further lemmas for lists and finite types used in the development

Definition Injective {A B} (f : A->B) :=
 forall x y, f x = f y -> x = y.

Lemma inductive_count (S:eqType) (Y:eqType) A (s:S) n (f: S -> Y):
Injective f -> count A s = n -> count (map (fun a:S => f a) A) (f s) = n.
intros inj. revert n. induction A; intros n HC.
- destruct n; try discriminate HC. reflexivity.
- simpl in *. decide (s=a). rewrite e in *. destruct n. discriminate HC. inversion HC.
  decide (f a = f a); try contradiction. rewrite (IHA n H0). now rewrite H0.
  decide (f s = f a). apply inj in e. contradiction. now apply IHA.

Lemma diff_constructors_count_zero (F X Y:eqType) (A: list F) (f: F -> X) (g: Y -> X) x:
(forall a b, f a <> g b) -> count (map (fun (a:F) => f a) A) (g x) = 0.
intros dis. induction A. auto. cbn. decide (g x = f a).
exfalso. apply (dis a x). symmetry. assumption. assumption.

Lemma in_count_app (X:eqType) (A B: list X) a:
  count (A++B) a = count A a + count B a.
  revert B a. induction A; intros B b; cbn. auto.
  decide (b = a); rewrite IHA; now cbn.

Section fix_X.
  Variable X:Type.
  Implicit Types (A B: list X) (a b c: X).

  Lemma last_app_eq A B a b :
    A++[a] = B++[b] -> A = B /\ a = b.
    intros H%(f_equal (@rev X)). rewrite !rev_app_distr in H. split.
    - inv H. apply (f_equal (@rev X)) in H2. now rewrite !rev_involutive in H2.
    - now inv H.

  Lemma rev_eq A B:
    List.rev A = List.rev B <-> A = B.
    - intros H%(f_equal (@rev X)). now rewrite !rev_involutive in H.
    - now intros <-.

  Lemma rev_nil A:
    rev A = [] -> A = [].
    destruct A. auto. now intros H%symmetry%app_cons_not_nil.

  Lemma map_inj (Y:Type) A B (f: X -> Y) :
    Injective f -> map f A = map f B <-> A = B.
    intros inj. split.
    - revert B. induction A; intros B H; cbn in *; destruct B; auto; cbn in H; inv H.
      rewrite (inj a x H1). specialize (IHA B H2). now subst.
    - now intros <-.
End fix_X.