Preliminaries

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.

Lists

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

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

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

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.

(* (** ** Decisions *) *)

(* 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). *)
(* Proof. *)
(*   unfold dec. decide equality.  *)
(* Defined. *)

Tactics

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

(* 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 *)
(*   end. *)

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

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.

Proof.
  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.
Qed.

(* (** ** Finite Types *) *)

(* (** The definitions of finite types are adopted from the Bachelor Thesis of Jan Menz. (https://www.ps.uni-saarland.de/~menz/bachelor.php) *) *)

(* (** 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. *)
(* Proof. *)
(*   induction A. *)
(*   - cbn. omega. *)
(*   - cbn. dec. *)
(*     + intros. left. symmetry. exact e. *)
(*     + intros. right. apply IHA. exact H. *)
(* Qed. *)

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

(* 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. *)
(* Proof. *)
(*   induction A. *)
(*   - reflexivity. *)
(*   - cbn. decide (x=a). *)
(*     +cbn. f_equal; exact IHA. *)
(*     + exact IHA. *)
(* Qed. *)

(* (** 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. *)
(* Proof. *)
(* 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. *)
(* Qed. *)

(* 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. *)
(* Proof. *)
(* intros dis. induction A. auto. cbn. decide (g x = f a). *)
(* exfalso. apply (dis a x). symmetry. assumption. assumption. *)
(* Qed. *)

(* Lemma notInZero (X: eqType) (x: X) A : *)
(*   not (x el A) <-> count A x = 0. *)
(* Proof. *)
(*   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. *)
(* Qed. *)

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.
  Proof.
    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.
  Qed.

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

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

  Lemma map_inj (Y:Type) A B (f: X -> Y) :
    Injective f -> map f A = map f B <-> A = B.
  Proof.
    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 <-.
  Qed.
End fix_X.

Lemma app_incl_l X (A B C : list X) :
  A ++ B <<= C -> A <<= C.
Proof.
  firstorder eauto.
Qed.

Lemma app_incl_R X (A B C : list X) :
  A ++ B <<= C -> B <<= C.
Proof.
  firstorder eauto.
Qed.

Lemma cons_incl X (a : X) (A B : list X) : a :: A <<= B -> A <<= B.
Proof.
  intros ? ? ?. eapply H. firstorder.
Qed.

Lemma incl_sing X (a : X) A : a el A -> [a] <<= A.
Proof.
  now intros ? ? [-> | [] ].
Qed.

Hint Resolve app_incl_l app_incl_R cons_incl incl_sing.

Hint Extern 4 (_ el map _ _) => eapply in_map_iff.
Hint Extern 4 (_ el filter _ _) => eapply filter_In.