Base Library for ICL

  • Version: 23 October 2016
  • Author: Gert Smolka, Saarland University
  • Acknowlegments: Sigurd Schneider, Dominik Kirst, Yannick Forster

Require Export Bool Omega List Setoid Morphisms.

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).
Definition equi X (A B : list X) : Prop := incl A B /\ incl B A.
Notation "A === B" := (equi A B) (at level 70).
Hint Unfold equi.

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

Hint Extern 4 => exact _. (* makes auto use type class inference *)

De Morgan laws

Lemma DM_or (X Y : Prop) :
  ~ (X \/ Y) <-> ~ X /\ ~ Y.
Proof.
  tauto.
Qed.

Lemma DM_exists X (p : X -> Prop) :
  ~ (exists x, p x) <-> forall x, ~ p x.
Proof.
  firstorder.
Qed.

Boolean propositions and decisions


Coercion bool2Prop (b : bool) := if b then True else False.

Lemma bool_Prop_true b :
  b = true -> b.
Proof.
  intros A. rewrite A. exact I.
Qed.

Lemma bool_Prop_false b :
  b = false -> ~ b.
Proof.
  intros A. rewrite A. cbn. auto.
Qed.

Hint Resolve bool_Prop_true bool_Prop_false.

Hint Extern 4 =>
match goal with
|[ H: False |- _ ] => destruct H
|[ H: ?s <> ?s |- _ ] => contradict H; reflexivity
|[ H: ~ bool2Prop true |- _ ] => destruct H
|[ H: bool2Prop false |- _ ] => destruct H
|[ H: true=false |- _ ] => discriminate H
|[ H: false=true |- _ ] => discriminate H
|[ H: ?b=false, H': bool2Prop(?b) |- _ ] => rewrite H in H'; destruct H'
|[ H: ?x el nil |- _ ] => destruct H
end.

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

Lemma Dec_reflect (X: Prop) (d: dec X) :
  Dec X <-> X.
Proof.
  destruct d as [A|A]; cbn; tauto.
Qed.

Notation Decb X := (dec2bool (Dec X)).

Lemma Dec_reflect_eq (X Y: Prop) (d: dec X) (e: dec Y) :
 Decb X = Decb Y <-> (X <-> Y).
Proof.
  destruct d as [D|D], e as [E|E]; cbn; intuition congruence.
Qed.

Lemma Dec_auto (X: Prop) (d: dec X) :
  X -> Dec X.
Proof.
  destruct d as [A|A]; cbn; tauto.
Qed.

Lemma Dec_auto_not (X: Prop) (d: dec X) :
  ~ X -> ~ Dec X.
Proof.
  destruct d as [A|A]; cbn; tauto.
Qed.

Hint Resolve Dec_auto Dec_auto_not.

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.

Decided propositions behave classically

Ltac contra A := (* proof by contradiction *)
  match goal with
  |[ |- ?t] => decide t as [A|A]; [exact A|exfalso]
  end.

Lemma dec_DN X :
  dec X -> ~~ X -> X.
Proof.
  unfold dec; tauto.
Qed.

Lemma dec_DM_and X Y :
  dec X -> dec Y -> ~ (X /\ Y) -> ~ X \/ ~ Y.
Proof.
  unfold dec; tauto.
Qed.

Lemma dec_DM_impl X Y :
  dec X -> dec Y -> ~ (X -> Y) -> X /\ ~ Y.
Proof.
  unfold dec; tauto.
Qed.

Propagation rules for decisions

Fact dec_transfer P Q :
  P <-> Q -> dec P -> dec Q.
Proof.
  unfold dec. tauto.
Qed.

Instance bool_dec (b: bool) :
  dec b.
Proof.
  unfold dec. destruct b; cbn; auto.
Qed.

Instance True_dec :
  dec True.
Proof.
  unfold dec; tauto.
Qed.

Instance False_dec :
  dec False.
Proof.
  unfold dec; tauto.
Qed.

Instance impl_dec (X Y : Prop) :
  dec X -> dec Y -> dec (X -> Y).
Proof.
  unfold dec; tauto.
Qed.

Instance and_dec (X Y : Prop) :
  dec X -> dec Y -> dec (X /\ Y).
Proof.
  unfold dec; tauto.
Qed.

Instance or_dec (X Y : Prop) :
  dec X -> dec Y -> dec (X \/ Y).
Proof.
  unfold dec; tauto.
Qed.

(* Coq standard modules make "not" and "iff" opaque for type class inference, 
   can be seen with Print HintDb typeclass_instances. *)


Instance not_dec (X : Prop) :
  dec X -> dec (~ X).
Proof.
  unfold not. auto.
Qed.

Instance iff_dec (X Y : Prop) :
  dec X -> dec Y -> dec (X <-> Y).
Proof.
  unfold iff. auto.
Qed.

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 bool_eq_dec :
  eq_dec bool.
Proof.
  unfold dec. decide equality.
Qed.

Instance nat_eq_dec :
  eq_dec nat.
Proof.
  unfold dec. decide equality.
Qed.

Instance prod_eq_dec X Y :
  eq_dec X -> eq_dec Y -> eq_dec (X * Y).
Proof.
  unfold dec. decide equality.
Qed.

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

Lists


(* Register additional simplification rules with autorewrite / simpl_list *)
(* Print Rewrite HintDb list. *)
Hint Rewrite <- app_assoc : list.
Hint Rewrite rev_app_distr map_app prod_length : list.

Lemma list_cycle (X : Type) (A : list X) x :
  x::A <> A.
Proof.
  intros B.
  assert (C: |x::A| <> |A|) by (cbn; omega).
  apply C. now rewrite B.
Qed.

Decisions for lists


Instance list_in_dec X (x : X) (A : list X) :
  eq_dec X -> dec (x el A).
Proof.
  intros D. apply in_dec. exact D.
Qed.

(* Certifying find *)

Lemma cfind X A (p: X -> Prop) (p_dec: forall x, dec (p x)) :
  {x | x el A /\ p x} + {forall x, x el A -> ~ p x}.
Proof.
  induction A as [|x A]; cbn.
  - tauto.
  - destruct IHA as [[y [D E]]|D].
    + eauto.
    + decide (p x) as [E|E].
      * left. eauto.
      * right. intros y [[]|F]; auto.
Qed.

Arguments cfind {X} A p {p_dec}.

Instance list_forall_dec X A (p : X -> Prop) :
  (forall x, dec (p x)) -> dec (forall x, x el A -> p x).
Proof.
  intros p_dec.
  destruct (cfind A (fun x => ~ p x)) as [[x [D E]]|D].
  - right. auto.
  - left. intros x E. apply dec_DN; auto.
Qed.

Instance list_exists_dec X A (p : X -> Prop) :
  (forall x, dec (p x)) -> dec (exists x, x el A /\ p x).
Proof.
  intros p_dec.
  destruct (cfind A p) as [[x [D E]]|D].
  - unfold dec. eauto.
  - right. intros [x [E F]]. exact (D x E F).
Qed.

Lemma list_exists_DM X A (p : X -> Prop) :
  (forall x, dec (p x)) ->
  ~ (forall x, x el A -> ~ p x) -> exists x, x el A /\ p x.
Proof.
  intros D E.
  destruct (cfind A p) as [F|F].
  + destruct F as [x F]. eauto.
  + contradiction (E F).
Qed.

Lemma list_exists_not_incl (X: eqType) (A B : list X) :
  ~ A <<= B -> exists x, x el A /\ ~ x el B.
Proof.
  intros E.
  apply list_exists_DM; auto.
  intros F. apply E. intros x G.
  apply dec_DN; auto.
Qed.

Lemma list_cc X (p : X -> Prop) A :
  (forall x, dec (p x)) ->
  (exists x, x el A /\ p x) -> {x | x el A /\ p x}.
Proof.
  intros D E.
  destruct (cfind A p) as [[x [F G]]|F].
  - eauto.
  - exfalso. destruct E as [x [G H]]. apply (F x); auto.
Qed.

Membership

We use the following lemmas from Coq's standard library List.
  • in_eq : x el x::A
  • in_nil : ~ x el nil
  • in_cons : x el A -> x el y::A
  • in_or_app : x el A \/ x el B -> x el A++B
  • in_app_iff : x el A++B <-> x el A \/ x el B
  • in_map_iff : y el map f A <-> exists x, f x = y /\ x el A

Hint Resolve in_eq in_nil in_cons in_or_app.

Section Membership.
  Variable X : Type.
  Implicit Types (x y: X) (A B: list X).

  Lemma in_cons_neq x y A :
    x el y::A -> x <> y -> x el A.
  Proof.
    cbn. intros [[]|D] E; congruence.
  Qed.

  Lemma not_in_cons x y A :
    ~ x el y :: A -> x <> y /\ ~ x el A.
  Proof.
    intuition; subst; auto.
  Qed.

End Membership.

Inclusion

We use the following lemmas from Coq's standard library List.
  • incl_refl : A <<= A
  • incl_tl : A <<= B -> A <<= x::B
  • incl_cons : x el B -> A <<= B -> x::A <<= B
  • incl_appl : A <<= B -> A <<= B++C
  • incl_appr : A <<= C -> A <<= B++C
  • incl_app : A <<= C -> B <<= C -> A++B <<= C

Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app.

Lemma incl_nil X (A : list X) :
  nil <<= A.

Proof. intros x []. Qed.

Hint Resolve incl_nil.

Lemma incl_map X Y A B (f : X -> Y) :
  A <<= B -> map f A <<= map f B.

Proof.
  intros D y E. apply in_map_iff in E as [x [E E']].
  subst y. apply in_map_iff. eauto.
Qed.

Section Inclusion.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma incl_nil_eq A :
    A <<= nil -> A=nil.
  Proof.
    intros D. destruct A as [|x A].
    - reflexivity.
    - exfalso. apply (D x). auto.
  Qed.

  Lemma nil_el_eq A :
    A = nil <-> forall x, ~x el A.
  Proof.
    split; intros H.
    - rewrite H. apply in_nil.
    - now apply incl_nil_eq.
  Qed.

  Lemma incl_shift x A B :
    A <<= B -> x::A <<= x::B.
  Proof. auto. Qed.

  Lemma incl_lcons x A B :
    x::A <<= B <-> x el B /\ A <<= B.
  Proof.
    split.
    - intros D. split; hnf; auto.
    - intros [D E] z [F|F]; subst; auto.
  Qed.

  Lemma incl_rcons x A B :
    A <<= x::B -> ~ x el A -> A <<= B.

  Proof. intros C D y E. destruct (C y E) as [F|F]; congruence. Qed.

  Lemma incl_lrcons x A B :
    x::A <<= x::B -> ~ x el A -> A <<= B.
  Proof.
    intros C D y E.
    assert (F: y el x::B) by auto.
    destruct F as [F|F]; congruence.
  Qed.

  Lemma incl_app_left A B C :
    A ++ B <<= C -> A <<= C /\ B <<= C.
  Proof.
    firstorder.
  Qed.

End Inclusion.

Definition inclp (X : Type) (A : list X) (p : X -> Prop) : Prop :=
  forall x, x el A -> p x.

Setoid rewriting with list inclusion and list equivalence


Instance incl_preorder X :
  PreOrder (@incl X).
Proof.
  constructor; hnf; unfold incl; auto.
Qed.

Instance equi_Equivalence X :
  Equivalence (@equi X).
Proof.
  constructor; hnf; firstorder.
Qed.

Instance incl_equi_proper X :
  Proper (@equi X ==> @equi X ==> iff) (@incl X).
Proof.
  hnf. intros A B D. hnf. firstorder.
Qed.

Instance cons_incl_proper X x :
  Proper (@incl X ==> @incl X) (@cons X x).
Proof.
  hnf. apply incl_shift.
Qed.

Instance cons_equi_proper X x :
  Proper (@equi X ==> @equi X) (@cons X x).
Proof.
  hnf. firstorder.
Qed.

Instance in_incl_proper X x :
  Proper (@incl X ==> Basics.impl) (@In X x).
Proof.
  intros A B D. hnf. auto.
Qed.

Instance in_equi_proper X x :
  Proper (@equi X ==> iff) (@In X x).
Proof.
  intros A B D. firstorder.
Qed.

Instance app_incl_proper X :
  Proper (@incl X ==> @incl X ==> @incl X) (@app X).
Proof.
  intros A B D A' B' E. auto.
Qed.

Instance app_equi_proper X :
  Proper (@equi X ==> @equi X ==> @equi X) (@app X).
Proof.
  hnf. intros A B D. hnf. intros A' B' E.
  destruct D, E; auto.
Qed.

Section Equi.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma equi_push x A :
    x el A -> A === x::A.
  Proof.
    auto.
  Qed.

  Lemma equi_dup x A :
    x::A === x::x::A.
  Proof.
    auto.
  Qed.

  Lemma equi_swap x y A:
    x::y::A === y::x::A.
  Proof.
    split; intros z; cbn; tauto.
  Qed.

End Equi.

Filter


Section Filter.
  Variable X : Type.
  Implicit Types (x y: X) (A B C: list X) (p q: X -> bool).

  Fixpoint filter p A : list X :=
    match A with
    | nil => nil
    | x::A' => if p x then x :: filter p A' else filter p A'
    end.

  Lemma in_filter_iff x p A :
    x el filter p A <-> x el A /\ p x.
  Proof.
    induction A as [|y A]; cbn.
    - tauto.
    - destruct (p y) eqn:E; cbn;
      rewrite IHA; intuition; subst; auto.
  Qed.

  Lemma filter_incl p A :
    filter p A <<= A.
  Proof.
    intros x D. apply in_filter_iff in D. apply D.
  Qed.

  Lemma filter_id p A :
    (forall x, x el A -> p x) -> filter p A = A.
  Proof.
    intros D.
    induction A as [|x A]; cbn.
    - reflexivity.
    - destruct (p x) eqn:E.
      + f_equal; auto.
      + exfalso. apply bool_Prop_false in E. auto.
  Qed.

  Lemma filter_app p A B :
    filter p (A ++ B) = filter p A ++ filter p B.
  Proof.
    induction A as [|y A]; cbn.
    - reflexivity.
    - rewrite IHA. destruct (p y); reflexivity.
  Qed.

  Lemma filter_fst p x A :
    p x -> filter p (x::A) = x::filter p A.
  Proof.
    cbn. destruct (p x); auto.
  Qed.

  Lemma filter_fst' p x A :
    ~ p x -> filter p (x::A) = filter p A.
  Proof.
    cbn. destruct (p x); auto.
  Qed.

End Filter.

Element removal


Section Removal.
  Variable X : eqType.
  Implicit Types (x y: X) (A B: list X).

  Definition rem A x : list X :=
    filter (fun z => Dec (z <> x)) A.

  Lemma in_rem_iff x A y :
    x el rem A y <-> x el A /\ x <> y.
  Proof.
    unfold rem. rewrite in_filter_iff, Dec_reflect. tauto.
  Qed.

  Lemma rem_not_in x y A :
    x = y \/ ~ x el A -> ~ x el rem A y.
  Proof.
    unfold rem. rewrite in_filter_iff, Dec_reflect. tauto.
  Qed.

  Lemma rem_incl A x :
    rem A x <<= A.
  Proof.
    apply filter_incl.
  Qed.

  Lemma rem_in x y A :
    x el rem A y -> x el A.
  Proof.
    apply rem_incl.
  Qed.

  Lemma rem_neq x y A :
    x <> y -> x el A -> x el rem A y.
  Proof.
    intros E F. apply in_rem_iff. auto.
  Qed.

  Lemma rem_equi x A :
    x::A === x::rem A x.
  Proof.
    split; intros y;
    intros [[]|E]; decide (x=y) as [[]|D];
    eauto using rem_in, rem_neq.
  Qed.

  Lemma rem_fst x A :
    rem (x::A) x = rem A x.
  Proof.
    unfold rem. rewrite filter_fst'; auto.
  Qed.

  Lemma rem_fst' x y A :
    x <> y -> rem (x::A) y = x::rem A y.
  Proof.
    intros E. unfold rem. rewrite filter_fst; auto.
  Qed.

End Removal.

Hint Resolve rem_not_in rem_incl rem_in rem_neq.