intial commit

Author: palmskog

.gitignore

@@ -0,0 +1,11 @@
+*.vo
+*.glob
+*.v.d
+Makefile.coq
+Makefile.coq.bak
+Makefile.coq.conf
+*~
+.coq-native/
+*.aux
+*.vio
+.coqdeps.d

_CoqProject

@@ -0,0 +1,9 @@
+clear.v
+eauto.v
+exists.v
+firstorder.v
+intros.v
+revert.v
+specialize.v
+subst.v
+symmetry.v

clear.v

@@ -0,0 +1,66 @@
+Require Import List.
+Import ListNotations.
+Require Import Sumbool.
+
+Ltac break_let :=
+  match goal with
+    | [ H : context [ (let (_,_) := ?X in _) ] |- _ ] => destruct X eqn:?
+    | [ |- context [ (let (_,_) := ?X in _) ] ] => destruct X eqn:?
+  end.
+
+Ltac find_injection :=
+  match goal with
+    | [ H : ?X _ _ = ?X _ _ |- _ ] => injection H; intros; subst
+  end.
+
+Ltac break_and :=
+  repeat match goal with
+           | [H : _ /\ _ |- _ ] => destruct H
+         end.
+
+Ltac break_if :=
+  match goal with
+    | [ |- context [ if ?X then _ else _ ] ] =>
+      match type of X with
+        | sumbool _ _ => destruct X
+        | _ => destruct X eqn:?
+      end
+  end.
+
+Definition update2 {A B : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (f : A -> A -> B) (x y : A) (v : B) :=
+  fun x' y' => if sumbool_and _ _ _ _ (A_eq_dec x x') (A_eq_dec y y') then v else f x' y'.
+
+Fixpoint collate {A B : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (from : A) (f : A -> A -> list B) (ms : list (A * B)) :=
+  match ms with
+   | [] => f
+   | (to, m) :: ms' => collate A_eq_dec from (update2 A_eq_dec f from to (f from to ++ [m])) ms'
+  end.
+
+Section Update2.
+  Variables A B : Type.
+  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}. 
+
+  Lemma collate_f_eq :
+    forall (f : A -> A -> list B) g h n n' l,
+      f n n' = g n n' ->
+      collate A_eq_dec h f l n n' = collate A_eq_dec h g l n n'.
+  Proof using.
+    intros f g h n n' l.
+    generalize f g; clear f g.
+    induction l; auto.
+    intros.
+    simpl in *.
+    break_let.
+    destruct a.
+    find_injection.
+    set (f' := update2 _ _ _ _ _).
+    set (g' := update2 _ _ _ _ _).
+    rewrite (IHl f' g'); auto.
+    unfold f', g', update2.
+    break_if; auto.
+    break_and.
+    subst.
+    rewrite H.
+    trivial.
+  Qed.
+End Update2.

eauto.v

@@ -0,0 +1,27 @@
+Require Import List.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+Section list_util.
+  Variables A : Type.
+
+  Lemma in_firstn : forall n (x : A) xs,
+      In x (firstn n xs) -> In x xs.
+  Proof using.
+    induction n; simpl; intuition.
+    destruct xs;simpl in *; intuition.
+  Qed.
+
+  Lemma firstn_NoDup : forall n (xs : list A),
+    NoDup xs ->
+    NoDup (firstn n xs).
+  Proof using.
+    induction n; intros; simpl; destruct xs; auto.
+    - apply NoDup_nil.
+    - inversion H; subst.
+      apply NoDup_cons.
+      * eauto 6 using in_firstn.
+      * apply IHn; auto.        
+  Qed.
+End list_util.

exists.v

@@ -0,0 +1,52 @@
+Require Import List.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+Fixpoint before {A: Type} (x : A) y l : Prop :=
+  match l with
+    | [] => False
+    | a :: l' =>
+      a = x \/
+      (a <> y /\ before x y l')
+  end.
+
+Section before.
+  Variable A : Type.
+
+  Lemma before_In :
+    forall x y l,
+      before (A:=A) x y l ->
+      In x l.
+  Proof using.
+    induction l; intros; simpl in *; intuition.
+  Qed.
+
+  Lemma before_split :
+    forall l (x y : A),
+      before x y l ->
+      x <> y ->
+      In x l ->
+      In y l ->
+      exists xs ys zs,
+        l = xs ++ x :: ys ++ y :: zs.
+  Proof using.
+    induction l; intros; simpl in *; intuition; subst; try congruence.
+    - exists []. simpl.
+      apply in_split in H1.
+      destruct H1; destruct H1.
+      subst. eauto.
+    - exists []. simpl.
+      apply in_split in H1.
+      destruct H1; destruct H1. subst. eauto.      
+    - exists []. simpl.
+      apply in_split in H1.
+      destruct H1; destruct H1. subst. eauto.      
+    - match goal with
+      | [ H : context [ In ], H' : context [ In ] |- _ ] =>
+      eapply H in H'
+      end; eauto.
+      destruct H1; destruct H1; destruct H1. subst.
+      exists (a :: x0), x1, x2. auto.
+  Qed.
+End before.

firstorder.v

@@ -0,0 +1,69 @@
+Require Import List.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+Fixpoint fin (n : nat) : Type :=
+  match n with
+    | 0 => False
+    | S n' => option (fin n')
+  end.
+
+Fixpoint fin_eq_dec (n : nat) : forall (a b : fin n), {a = b} + {a <> b}.
+  refine
+   (match n with
+      | 0 => fun a b : fin 0 => right (match b with end)
+      | S n' => fun a b : fin (S n') =>
+                 match a, b with
+                   | Some a', Some b' =>
+                     match fin_eq_dec n' a' b' with
+                       | left _ _ => left _
+                       | right _ _ => right _
+                     end
+                   | Some a', None => right _
+                   | None, Some b' => right _
+                   | None, None => left eq_refl
+                 end
+    end); congruence.
+Defined.
+
+Fixpoint all_fin (n : nat) : list (fin n) :=
+  match n with
+    | 0 => []
+    | S n' => None :: map (fun x => Some x) (all_fin n')
+  end.
+
+Lemma all_fin_all :
+  forall n (x : fin n),
+    In x (all_fin n).
+Proof.
+  induction n; intros.
+  - inversion x.
+  - simpl in *. destruct x; auto using in_map.
+Qed.
+
+Lemma NoDup_map_injective : forall A B (f : A -> B) xs,
+    (forall x y, In x xs -> In y xs ->
+            f x = f y -> x = y) ->
+    NoDup xs -> NoDup (map f xs).
+Proof using.
+  induction xs; intros.
+  - constructor.
+  - simpl. inversion H0. subst. constructor.
+    + intro.
+      apply in_map_iff in H1.      
+      destruct H1.
+      destruct H1.
+      assert (x = a) by intuition.
+      subst.
+      congruence.
+    + intuition.
+Qed.
+
+Lemma all_fin_NoDup :
+  forall n, NoDup (all_fin n).
+Proof.
+  induction n; intros; simpl; constructor.
+  - intro. apply in_map_iff in H. firstorder. discriminate.
+  - apply NoDup_map_injective; auto. congruence.
+Qed.

intros.v

@@ -0,0 +1,37 @@
+Require Import List.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+Section list_util.
+  Variables A B : Type.
+  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.
+
+  Lemma In_cons_neq :
+    forall a x xs,
+      In(A:=A) a (x :: xs) ->
+      a <> x ->
+      In a xs.
+  Proof using.
+    simpl.
+    intuition congruence.
+  Qed.
+
+  Lemma in_fold_left_by_cons_in :
+    forall (l : list B) (g : B -> A) x acc,
+      In x (fold_left (fun a b => g b :: a) l acc) ->
+      In x acc \/ exists y, In y l /\ x = g y.
+  Proof using A_eq_dec.
+    intros until l.
+    induction l.
+    - auto.
+    - simpl; intros.
+      destruct (A_eq_dec x (g a)); subst.
+      + right; exists a; tauto.
+      + apply IHl in H.
+        case H; [left|right].
+        * apply In_cons_neq in H0; tauto.
+        * destruct H0; destruct H0.
+          exists x0; split; auto.
+  Qed.
+End list_util.

revert.v

@@ -0,0 +1,48 @@
+Require Import List.
+Import ListNotations.
+Require Import Sumbool.
+
+Ltac break_and :=
+  repeat match goal with
+           | [H : _ /\ _ |- _ ] => destruct H
+         end.
+
+Ltac break_if :=
+  match goal with
+    | [ |- context [ if ?X then _ else _ ] ] =>
+      match type of X with
+        | sumbool _ _ => destruct X
+        | _ => destruct X eqn:?
+      end
+  end.
+
+Definition update2 {A B : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (f : A -> A -> B) (x y : A) (v : B) :=
+  fun x' y' => if sumbool_and _ _ _ _ (A_eq_dec x x') (A_eq_dec y y') then v else f x' y'.
+
+Fixpoint collate {A B : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (from : A) (f : A -> A -> list B) (ms : list (A * B)) :=
+  match ms with
+   | [] => f
+   | (to, m) :: ms' => collate A_eq_dec from (update2 A_eq_dec f from to (f from to ++ [m])) ms'
+  end.
+
+Section Update2.
+  Variables A B : Type.
+  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}. 
+
+  Lemma collate_neq :
+    forall h n n' ns (f : A -> A -> list B),
+      h <> n ->
+      collate A_eq_dec h f ns n n' = f n n'.
+  Proof using.
+    intros.
+    revert f.
+    induction ns; intros; auto.
+    destruct a.
+    simpl in *.
+    rewrite IHns.
+    unfold update2.
+    break_if; auto.
+    break_and; subst.
+    intuition.
+  Qed.
+End Update2.

specialize.v

@@ -0,0 +1,58 @@
+Require Import List.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+Ltac break_match :=
+  match goal with
+    | [ |- context [ match ?X with _ => _ end ] ] =>
+      match type of X with
+        | sumbool _ _ => destruct X
+        | _ => destruct X eqn:?
+      end
+  end.
+
+Ltac do_in_app :=
+  match goal with
+    | [ H : In _ (_ ++ _) |- _ ] => apply in_app_iff in H
+  end.
+
+Section dedup.
+  Variable A : Type.
+  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.
+
+  Fixpoint dedup (xs : list A) : list A :=
+    match xs with
+    | [] => []
+    | x :: xs => let tail := dedup xs in
+                 if in_dec A_eq_dec x xs then
+                   tail
+                 else
+                   x :: tail
+    end.
+
+  Lemma dedup_app : forall (xs ys : list A),
+      (forall x y, In x xs -> In y ys -> x <> y) ->
+      dedup (xs ++ ys) = dedup xs ++ dedup ys.
+  Proof using.
+    intros. induction xs; simpl; auto.
+    repeat break_match.
+    - apply IHxs.
+      intros.
+      apply H; intuition.
+    - exfalso.
+      specialize (H a a).
+      apply H; intuition.
+      do_in_app.
+      intuition.
+    - exfalso.
+      apply n.
+      intuition.
+    - simpl.
+      f_equal.
+      apply IHxs.
+      intros.
+      apply H; intuition.
+  Qed.
+
+End dedup.