diff --git a/.lia.cache b/.lia.cache
new file mode 100644
index 0000000..85baaf2
Binary files /dev/null and b/.lia.cache differ
diff --git a/Auto.v b/Auto.v
new file mode 100644
index 0000000..618a780
--- /dev/null
+++ b/Auto.v
@@ -0,0 +1,27 @@
+From Coq Require Import Arith List.
+From Coq Require Import Lia.
+Require Import Ring.
+
+Theorem plus_id_exercise : forall n m o : nat,
+    n = m -> m = o -> n + m = m + o.
+Proof.
+  lia.
+Qed.
+
+Theorem add_assoc : forall n m p : nat,
+    n + (m + p) = (n + m) + p.
+Proof.
+  lia.
+Qed.
+
+Theorem S_injective : forall (n m : nat),
+    S n = S m -> n = m.
+Proof.
+  congruence.
+Qed.
+
+Theorem or_distributes_over_and : forall P Q R : Prop,
+    P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
+Proof.
+  intuition.
+Qed.
diff --git a/Auto.v~ b/Auto.v~
new file mode 100644
index 0000000..1464cae
--- /dev/null
+++ b/Auto.v~
@@ -0,0 +1 @@
+From Coq Require Import Arith List.
diff --git a/Imp.v b/Imp.v
new file mode 100644
index 0000000..3f3c428
--- /dev/null
+++ b/Imp.v
@@ -0,0 +1,498 @@
+From Coq Require Import Bool.Bool.
+From Coq Require Import Init.Nat.
+From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.EqNat. Import Nat.
+From Coq Require Import Lia.
+From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import Strings.String.
+From LF Require Import Maps.
+Set Default Goal Selector "!".
+
+Inductive aexp : Type :=
+| ANum (n : nat)
+| AId (x : string)
+| APlus (a1 a2 : aexp)
+| AMinus (a1 a2 : aexp)
+| AMult (a1 a2 : aexp).
+
+Definition W : string := "W".
+Definition X : string := "X".
+Definition Y : string := "Y".
+Definition Z : string := "Z".
+
+Inductive bexp : Type :=
+| BTrue
+| BFalse
+| BEq (a1 a2 : aexp)
+| BNeq (a1 a2 : aexp)
+| BLe (a1 a2 : aexp)
+| BGt (a1 a2 : aexp)
+| BNot (b : bexp)
+| BAnd (b1 b2 : bexp).
+
+Coercion AId : string >-> aexp.
+Coercion ANum : nat >-> aexp.
+Declare Custom Entry com.
+Declare Scope com_scope.
+Declare Custom Entry com_aux.
+Notation "<{ e }>" := e (e custom com_aux) : com_scope.
+Notation "e" := e (in custom com_aux at level 0, e custom com) : com_scope.
+Notation "( x )" := x (in custom com, x at level 99) : com_scope.
+Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
+Notation "f x .. y" := (.. (f x) .. y)
+                         (in custom com at level 0, only parsing,
+                             f constr at level 0, x constr at level 9,
+                             y constr at level 9) : com_scope.
+Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
+Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity).
+Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity).
+Notation "'true'" := true (at level 1).
+Notation "'true'" := BTrue (in custom com at level 0).
+Notation "'false'" := false (at level 1).
+Notation "'false'" := BFalse (in custom com at level 0).
+Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity).
+Notation "x > y" := (BGt x y) (in custom com at level 70, no associativity).
+Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity).
+Notation "x <> y" := (BNeq x y) (in custom com at level 70, no associativity).
+Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity).
+Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity).
+Open Scope com_scope.
+
+Definition example_aexp : aexp := <{ 3 + (X * 2) }>.
+Definition example_bexp := <{ true && ~(X <= 4) }>.
+
+Definition state := total_map nat.
+
+Fixpoint aeval (st : state) (a : aexp) : nat :=
+  match a with
+  | ANum n => n
+  | AId x => st x
+  | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
+  | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
+  | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
+  end.
+
+Definition empty_st := (_ !-> 0).
+
+Example test_aeval1 :
+  aeval empty_st <{2 + 2}> = 4.
+Proof. reflexivity. Qed.
+
+Fixpoint beval (st : state) (b : bexp) : bool :=
+  match b with
+  | <{true}> => true
+  | <{false}> => false
+  | <{a1 = a2}> => (aeval st a1) =? (aeval st a2)
+  | <{a1 <> a2}> => negb ((aeval st a1) =? (aeval st a2))
+  | <{a1 <= a2}> => (aeval st a1) <=? (aeval st a2)
+  | <{a1 > a2}> => negb ((aeval st a1) <=? (aeval st a2))
+  | <{~ b1}> => negb (beval st b1)
+  | <{b1 && b2}> => andb (beval st b1) (beval st b2)
+  end.
+
+Notation "x '!->' v" := (x !-> v ; empty_st) (at level 100).
+
+Example aexp1 :
+  aeval (X !-> 5) <{ 3 + (X * 2) }> = 13.
+Proof.
+  reflexivity. Qed.
+
+Inductive com : Type :=
+| CSkip
+| CAsgn (x : string) (a : aexp)
+| CSeq (c1 c2 : com)
+| CIf (b : bexp) (c1 c2 : com)
+| CWhile (b : bexp) (c : com).
+
+Notation "'skip'"  :=
+  CSkip (in custom com at level 0) : com_scope.
+Notation "x := y"  :=
+  (CAsgn x y)
+    (in custom com at level 0, x constr at level 0,
+        y at level 85, no associativity) : com_scope.
+Notation "x ; y" :=
+  (CSeq x y)
+    (in custom com at level 90,
+        right associativity) : com_scope.
+Notation "'if' x 'then' y 'else' z 'end'" :=
+  (CIf x y z)
+    (in custom com at level 89, x at level 99,
+        y at level 99, z at level 99) : com_scope.
+Notation "'while' x 'do' y 'end'" :=
+  (CWhile x y)
+    (in custom com at level 89, x at level 99,
+        y at level 99) : com_scope.
+
+Reserved Notation "st '=[' c ']=>' st'"
+  (at level 40, c custom com at level 99, st' constr at next level).
+
+Inductive ceval : com -> state -> state -> Prop :=
+| E_Skip : forall st,
+    st =[ skip ]=> st
+| E_Asgn : forall st a n x,
+    aeval st a = n -> st =[ x := a ]=> (x !-> n ; st)
+| E_Seq : forall c1 c2 st st' st'',
+    st =[ c1 ]=> st' ->
+                 st' =[ c2 ]=> st'' ->
+                               st =[ c1 ; c2 ]=> st''
+| E_IfTrue : forall st st' b c1 c2,
+    beval st b = true ->
+    st =[ c1 ]=> st' ->
+                 st =[ if b then c1 else c2 end]=> st'
+| E_IfFalse : forall st st' b c1 c2,
+    beval st b = false ->
+    st =[ c2 ]=> st' ->
+                 st =[ if b then c1 else c2 end]=> st'
+| E_WhileFalse : forall b st c,
+    beval st b = false ->
+    st =[ while b do c end ]=> st
+| E_WhileTrue : forall st st' st'' b c,
+    beval st b = true ->
+    st =[ c ]=> st' ->
+                st' =[ while b do c end ]=> st'' ->
+                                            st =[ while b do c end ]=> st''
+
+where "st =[ c ]=> st'" := (ceval c st st').
+
+Example ceval_example1 :
+  empty_st =[
+      X := 2;
+      if (X <= 1)
+      then Y := 3
+      else Z := 4
+      end
+    ]=> (Z !-> 4 ; X !-> 2).
+Proof.
+  apply E_Seq with (X !-> 2).
+  - apply E_Asgn. reflexivity.
+  - apply E_IfFalse.
+    + reflexivity.
+    + apply E_Asgn.
+      reflexivity.
+Qed.
+
+Example ceval_example2 :
+  empty_st =[
+      X := 0;
+      Y := 1;
+      Z := 2
+    ]=> (Z !-> 2 ; Y !-> 1 ; X !-> 0).
+Proof.
+  apply E_Seq with (X !-> 0).
+  { apply E_Asgn. reflexivity. }
+  apply E_Seq with (Y !-> 1 ; X !-> 0).
+  { apply E_Asgn. reflexivity. }
+  apply E_Asgn. reflexivity.
+Qed.
+
+Definition pup_to_n : com :=
+  <{ while X <> 0 do
+                    Y := Y + X;
+                    X := X - 1
+                    end
+    }>.
+
+Theorem pup_to_2_ceval :
+  (X !-> 2) =[
+      pup_to_n
+    ]=> (X !-> 0 ; Y !-> 3 ; X !-> 1 ; Y !-> 2 ; X !-> 2).
+Proof.
+  apply E_WhileTrue with (X !-> 1 ; Y !-> 2 ; X !-> 2).
+  { reflexivity. }
+  { apply E_Seq with (Y !-> 2 ; X !-> 2).
+    { apply E_Asgn. reflexivity. }
+    apply E_Asgn. reflexivity. }
+  apply E_WhileTrue with (X !-> 0 ; Y !-> 3 ; X !-> 1 ; Y !-> 2 ; X !-> 2).
+  { reflexivity. }
+  { apply E_Seq with (Y !-> 3 ; X !-> 1 ; Y !-> 2 ; X !-> 2).
+    { apply E_Asgn. reflexivity. }
+    apply E_Asgn. reflexivity. }
+
+  apply E_WhileFalse.
+  reflexivity.
+Qed.
+
+Theorem ceval_deterministic : forall c st st1 st2,
+    st =[ c ]=> st1 ->
+                st =[ c ]=> st2 ->
+                            st1 = st2.
+Proof.
+  intros c st st1 st2 E1 E2.
+  generalize dependent st2.
+  induction E1; intros st2 E2; inversion E2; subst.
+  - reflexivity.
+  - reflexivity.
+  - rewrite (IHE1_1 st'0 H1) in *.
+    apply IHE1_2.
+    assumption.
+  - apply IHE1. assumption.
+  - rewrite H in H5. discriminate.
+  - rewrite H in H5. discriminate.
+  - apply IHE1. assumption.
+  - reflexivity.
+  - rewrite H in H2. discriminate.
+  - rewrite H in H4. discriminate.
+  - rewrite (IHE1_1 st'0 H3) in *.
+    apply IHE1_2. assumption. Qed.
+
+Definition plus2 : com :=
+  <{ X := X + 2 }>.
+
+Theorem plus2_spec : forall st n st',
+    st X = n ->
+    st =[ plus2 ]=> st' ->
+                    st' X = n + 2.
+Proof.
+  intros st n st' HX Heval.
+  inversion Heval.
+  subst. clear Heval. simpl.
+  apply t_update_eq.
+Qed.
+
+Definition XtimesYinZ : com :=
+  <{ Z := X * Y }>.
+
+Theorem XtimesYinZ_spec : forall st n m st',
+    st X = n ->
+    st Y = m ->
+    st =[ XtimesYinZ ]=> st' ->
+                         st' Z = n * m.
+Proof.
+  intros st n m st' HX HY Heval.
+  inversion Heval.
+  subst.
+  simpl.
+  apply t_update_eq.
+Qed.
+
+Definition loop : com :=
+  <{ while true do
+         skip
+         end }>.
+
+Theorem loop_never_stops : forall st st',
+    ~(st =[ loop ]=> st').
+Proof.
+  intros st st' contra.
+  unfold loop in contra.
+  remember <{ while true do skip end }> as loopdef eqn:Heqloopdef.
+  induction contra ; try discriminate.
+  - inversion Heqloopdef; subst.
+    simpl in H.
+    discriminate.
+  - inversion Heqloopdef; subst.
+    apply IHcontra2.
+    reflexivity.
+Qed.
+
+Fixpoint no_whiles (c : com) : bool :=
+  match c with
+  | <{ skip }> => true
+  | <{ _ := _ }> => true
+  | <{ c1 ; c2 }> =>
+      andb (no_whiles c1) (no_whiles c2)
+  | <{ if _ then ct else cf end }> =>
+      andb (no_whiles ct) (no_whiles cf)
+  | <{ while _ do _ end }> => false
+  end.
+
+Inductive no_whilesR : com -> Prop :=
+| no_whilesSkip : no_whilesR <{ skip }>
+| no_whilesAsgn (x : string) (a : aexp) : no_whilesR <{ x := a }>
+| no_whilesSeq (c1 c2 : com) (H1 : no_whilesR c1) (H2 : no_whilesR c2) :
+  no_whilesR <{ c1 ; c2 }>
+| no_whilesIf (b : bexp) (ct cf : com) (H1 : no_whilesR ct) (H2 : no_whilesR cf) :
+  no_whilesR <{ if b then ct else cf end }>.
+
+Theorem no_whiles_eqv:
+  forall c, no_whiles c = true <-> no_whilesR c.
+Proof.
+  intros c.
+  split.
+  - intros H.
+    induction c;
+      try (constructor ; reflexivity) ;
+      try (constructor ;
+           [ apply IHc1 ; reflexivity
+           | apply IHc2 ; reflexivity ]) ;
+      try (constructor ; [ apply IHc1 | apply IHc2 ] ;
+           inversion H;
+           apply andb_true_iff
+             with (b1 := no_whiles c1)
+                  (b2 := no_whiles c2)
+             in H1 as [G1 G2];
+           rewrite G1;
+           rewrite G2;
+           reflexivity).
+    + simpl in H. discriminate.
+  - intros H.
+    induction H;
+      try reflexivity;
+      try (simpl; rewrite IHno_whilesR1;
+           rewrite IHno_whilesR2; reflexivity).
+Qed.
+
+Theorem no_whiles_terminating : forall (st : state) (c : com),
+    no_whilesR c -> exists (st' : state),
+      st =[ c ]=> st'.
+Proof.
+  intros st c H.
+  generalize dependent st.
+  induction c.
+  - intros.
+    exists st.
+    constructor.
+  - intros.
+    exists (x !-> (aeval st a) ; st).
+    constructor.
+    reflexivity.
+  - intros.
+    inversion H.
+    subst.
+    apply IHc1 with (st := st) in H0.
+    destruct H0 as [st' H1].
+    apply IHc2 with (st := st') in H3.
+    destruct H3 as [st'' H2].
+    exists st''.
+    apply (E_Seq c1 c2 st st' st'' H1 H2).
+  - intros.
+    inversion H.
+    subst.
+    destruct (beval st b) eqn:Eb ;
+      [ apply IHc1 with (st := st) in H0 as G
+      | apply IHc2 with (st := st) in H4 as G] ;
+      destruct G as [st' G1] ;
+      exists st' ;
+      constructor ;
+      assumption.
+  - intros.
+    inversion H.
+Qed.
+
+
+Inductive sinstr : Type :=
+| SPush (n : nat)
+| SLoad (x : string)
+| SPlus
+| SMinus
+| SMult.
+
+Fixpoint s_execute (st : state) (stack : list nat)
+  (prog : list sinstr)
+  : list nat :=
+  match prog with
+  | [] => stack
+  | (SPush n :: rest) => s_execute st (n :: stack) rest
+  | (SLoad x :: rest) => s_execute st (st x :: stack) rest
+  | (SPlus :: rest) => match stack with
+                       | x :: y :: ss =>
+                           s_execute st ((y + x) :: ss) rest
+                       | _ => s_execute st stack rest
+                       end
+  | (SMinus :: rest) => match stack with
+                        | x :: y :: ss =>
+                            s_execute st ((y - x) :: ss) rest
+                        | _ => s_execute st stack rest
+                        end
+  | (SMult :: rest) => match stack with
+                       | x :: y :: ss =>
+                           s_execute st ((y * x) :: ss) rest
+                       | _ => s_execute st stack rest
+                       end
+  end.
+
+Example s_execute1 :
+  s_execute empty_st []
+    [SPush 5; SPush 3; SPush 1; SMinus]
+  = [2; 5].
+Proof. reflexivity. Qed.
+
+Fixpoint s_compile (e : aexp) : list sinstr :=
+  match e with
+  | ANum n => [SPush n]
+  | AId x => [SLoad x]
+  | APlus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SPlus]
+  | AMinus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMinus]
+  | AMult a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMult]
+  end.
+
+Example s_compile1 :
+  s_compile <{ X - (2 * Y) }>
+  = [SLoad X; SPush 2; SLoad Y; SMult; SMinus].
+Proof. reflexivity.
+Qed.
+
+Theorem execute_app : forall st p1 p2 stack,
+    s_execute st stack (p1 ++ p2) = s_execute st (s_execute st stack p1) p2.
+Proof.
+  intros st p1 p2.
+  induction p1.
+  - intros.
+    reflexivity.
+  - intros.
+    destruct a; simpl.
+    + apply (IHp1 (n :: stack)).
+    + apply (IHp1 (st x :: stack)).
+    + destruct stack.
+      { apply IHp1. }
+      destruct stack.
+      { apply IHp1. }
+      apply (IHp1 (n0 + n :: stack)).
+    + destruct stack.
+      { apply IHp1. }
+      destruct stack.
+      { apply IHp1. }
+      apply (IHp1 (n0 - n :: stack)).
+    + destruct stack.
+      { apply IHp1. }
+      destruct stack.
+      { apply IHp1. }
+      apply (IHp1 (n0 * n :: stack)).
+Qed.
+
+Lemma s_compile_correct_aux : forall st e stack,
+    s_execute st stack (s_compile e) = aeval st e :: stack.
+Proof.
+  intros st e.
+  generalize dependent st.
+  induction e; intros; try reflexivity;
+    try (simpl;
+         rewrite execute_app;
+         rewrite execute_app;
+         rewrite (IHe1 st stack);
+         rewrite (IHe2 st (aeval st e1 :: stack));
+         reflexivity).
+Qed.
+
+Theorem s_compile_correct : forall (st : state) (e : aexp),
+    s_execute st [] (s_compile e) = [ aeval st e ].
+Proof.
+  intros.
+  apply (s_compile_correct_aux st e []).
+Qed.
+
+Fixpoint beval' (st : state) (b : bexp) : bool :=
+  match b with
+  | <{true}> => true
+  | <{false}> => false
+  | <{a1 = a2}> => (aeval st a1) =? (aeval st a2)
+  | <{a1 <> a2}> => negb ((aeval st a1) =? (aeval st a2))
+  | <{a1 <= a2}> => (aeval st a1) <=? (aeval st a2)
+  | <{a1 > a2}> => negb ((aeval st a1) <=? (aeval st a2))
+  | <{~ b1}> => negb (beval st b1)
+  | <{b1 && b2}> => if (negb (beval' st b1))
+                    then false
+                    else beval' st b2
+  end.
+
+Theorem beval_beval'_equiv: forall (st : state) (b : bexp),
+    beval st b = beval' st b.
+Proof.
+  intros.
+  induction b;
+    try reflexivity.
+  - simpl.
+    rewrite IHb1.
+    rewrite IHb2.
+    destruct (beval' st b1); reflexivity.
+Qed.
diff --git a/Imp.v~ b/Imp.v~
new file mode 100644
index 0000000..eaf144a
--- /dev/null
+++ b/Imp.v~
@@ -0,0 +1,441 @@
+From Coq Require Import Bool.Bool.
+From Coq Require Import Init.Nat.
+From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.EqNat. Import Nat.
+From Coq Require Import Lia.
+From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import Strings.String.
+From LF Require Import Maps.
+Set Default Goal Selector "!".
+
+Module AExp.
+
+  Inductive aexp : Type :=
+  | ANum (n : nat)
+  | AId (x : string)
+  | APlus (a1 a2 : aexp)
+  | AMinus (a1 a2 : aexp)
+  | AMult (a1 a2 : aexp).
+
+  Definition W : string := "W".
+  Definition X : string := "X".
+  Definition Y : string := "Y".
+  Definition Z : string := "Z".
+
+  Inductive bexp : Type :=
+  | BTrue
+  | BFalse
+  | BEq (a1 a2 : aexp)
+  | BNeq (a1 a2 : aexp)
+  | BLe (a1 a2 : aexp)
+  | BGt (a1 a2 : aexp)
+  | BNot (b : bexp)
+  | BAnd (b1 b2 : bexp).
+
+  Coercion AId : string >-> aexp.
+  Coercion ANum : nat >-> aexp.
+  Declare Custom Entry com.
+  Declare Scope com_scope.
+  Declare Custom Entry com_aux.
+  Notation "<{ e }>" := e (e custom com_aux) : com_scope.
+  Notation "e" := e (in custom com_aux at level 0, e custom com) : com_scope.
+  Notation "( x )" := x (in custom com, x at level 99) : com_scope.
+  Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
+  Notation "f x .. y" := (.. (f x) .. y)
+                           (in custom com at level 0, only parsing,
+                               f constr at level 0, x constr at level 9,
+                               y constr at level 9) : com_scope.
+  Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
+  Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity).
+  Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity).
+  Notation "'true'" := true (at level 1).
+  Notation "'true'" := BTrue (in custom com at level 0).
+  Notation "'false'" := false (at level 1).
+  Notation "'false'" := BFalse (in custom com at level 0).
+  Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity).
+  Notation "x > y" := (BGt x y) (in custom com at level 70, no associativity).
+  Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity).
+  Notation "x <> y" := (BNeq x y) (in custom com at level 70, no associativity).
+  Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity).
+  Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity).
+  Open Scope com_scope.
+
+  Definition example_aexp : aexp := <{ 3 + (X * 2) }>.
+  Definition example_bexp := <{ true && ~(X <= 4) }>.
+
+  Definition state := total_map nat.
+
+  Fixpoint aeval (st : state) (a : aexp) : nat :=
+    match a with
+    | ANum n => n
+    | AId x => st x
+    | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
+    | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
+    | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
+    end.
+
+  Definition empty_st := (_ !-> 0).
+
+  Example test_aeval1 :
+    aeval empty_st <{2 + 2}> = 4.
+  Proof. reflexivity. Qed.
+
+  Fixpoint beval (st : state) (b : bexp) : bool :=
+    match b with
+    | <{true}> => true
+    | <{false}> => false
+    | <{a1 = a2}> => (aeval st a1) =? (aeval st a2)
+    | <{a1 <> a2}> => negb ((aeval st a1) =? (aeval st a2))
+    | <{a1 <= a2}> => (aeval st a1) <=? (aeval st a2)
+    | <{a1 > a2}> => negb ((aeval st a1) <=? (aeval st a2))
+    | <{~ b1}> => negb (beval st b1)
+    | <{b1 && b2}> => andb (beval st b1) (beval st b2)
+    end.
+
+  Notation "x '!->' v" := (x !-> v ; empty_st) (at level 100).
+
+  Example aexp1 :
+    aeval (X !-> 5) <{ 3 + (X * 2) }> = 13.
+  Proof.
+    reflexivity. Qed.
+
+  Inductive com : Type :=
+  | CSkip
+  | CAsgn (x : string) (a : aexp)
+  | CSeq (c1 c2 : com)
+  | CIf (b : bexp) (c1 c2 : com)
+  | CWhile (b : bexp) (c : com).
+
+  Notation "'skip'"  :=
+    CSkip (in custom com at level 0) : com_scope.
+  Notation "x := y"  :=
+    (CAsgn x y)
+      (in custom com at level 0, x constr at level 0,
+          y at level 85, no associativity) : com_scope.
+  Notation "x ; y" :=
+    (CSeq x y)
+      (in custom com at level 90,
+          right associativity) : com_scope.
+  Notation "'if' x 'then' y 'else' z 'end'" :=
+    (CIf x y z)
+      (in custom com at level 89, x at level 99,
+          y at level 99, z at level 99) : com_scope.
+  Notation "'while' x 'do' y 'end'" :=
+    (CWhile x y)
+      (in custom com at level 89, x at level 99,
+          y at level 99) : com_scope.
+
+  Reserved Notation "st '=[' c ']=>' st'"
+    (at level 40, c custom com at level 99, st' constr at next level).
+
+  Inductive ceval : com -> state -> state -> Prop :=
+  | E_Skip : forall st,
+      st =[ skip ]=> st
+  | E_Asgn : forall st a n x,
+      aeval st a = n -> st =[ x := a ]=> (x !-> n ; st)
+  | E_Seq : forall c1 c2 st st' st'',
+      st =[ c1 ]=> st' ->
+      st' =[ c2 ]=> st'' ->
+      st =[ c1 ; c2 ]=> st''
+  | E_IfTrue : forall st st' b c1 c2,
+      beval st b = true ->
+      st =[ c1 ]=> st' ->
+      st =[ if b then c1 else c2 end]=> st'
+  | E_IfFalse : forall st st' b c1 c2,
+      beval st b = false ->
+      st =[ c2 ]=> st' ->
+      st =[ if b then c1 else c2 end]=> st'
+  | E_WhileFalse : forall b st c,
+      beval st b = false ->
+      st =[ while b do c end ]=> st
+  | E_WhileTrue : forall st st' st'' b c,
+      beval st b = true ->
+      st =[ c ]=> st' ->
+      st' =[ while b do c end ]=> st'' ->
+      st =[ while b do c end ]=> st''
+
+  where "st =[ c ]=> st'" := (ceval c st st').
+
+  Example ceval_example1 :
+    empty_st =[
+        X := 2;
+        if (X <= 1)
+            then Y := 3
+            else Z := 4
+        end
+    ]=> (Z !-> 4 ; X !-> 2).
+  Proof.
+    apply E_Seq with (X !-> 2).
+    - apply E_Asgn. reflexivity.
+    - apply E_IfFalse.
+      + reflexivity.
+      + apply E_Asgn.
+        reflexivity.
+  Qed.
+
+  Example ceval_example2 :
+    empty_st =[
+        X := 0;
+        Y := 1;
+        Z := 2
+      ]=> (Z !-> 2 ; Y !-> 1 ; X !-> 0).
+  Proof.
+    apply E_Seq with (X !-> 0).
+    { apply E_Asgn. reflexivity. }
+    apply E_Seq with (Y !-> 1 ; X !-> 0).
+    { apply E_Asgn. reflexivity. }
+    apply E_Asgn. reflexivity.
+  Qed.
+
+  Definition pup_to_n : com :=
+    <{ while X <> 0 do
+           Y := Y + X;
+           X := X - 1
+       end
+      }>.
+
+  Theorem pup_to_2_ceval :
+    (X !-> 2) =[
+        pup_to_n
+      ]=> (X !-> 0 ; Y !-> 3 ; X !-> 1 ; Y !-> 2 ; X !-> 2).
+  Proof.
+    apply E_WhileTrue with (X !-> 1 ; Y !-> 2 ; X !-> 2).
+    { reflexivity. }
+    { apply E_Seq with (Y !-> 2 ; X !-> 2).
+      { apply E_Asgn. reflexivity. }
+      apply E_Asgn. reflexivity. }
+    apply E_WhileTrue with (X !-> 0 ; Y !-> 3 ; X !-> 1 ; Y !-> 2 ; X !-> 2).
+    { reflexivity. }
+    { apply E_Seq with (Y !-> 3 ; X !-> 1 ; Y !-> 2 ; X !-> 2).
+      { apply E_Asgn. reflexivity. }
+      apply E_Asgn. reflexivity. }
+
+    apply E_WhileFalse.
+    reflexivity.
+  Qed.
+
+  Theorem ceval_deterministic : forall c st st1 st2,
+      st =[ c ]=> st1 ->
+      st =[ c ]=> st2 ->
+      st1 = st2.
+  Proof.
+    intros c st st1 st2 E1 E2.
+    generalize dependent st2.
+    induction E1; intros st2 E2; inversion E2; subst.
+    - reflexivity.
+    - reflexivity.
+    - rewrite (IHE1_1 st'0 H1) in *.
+      apply IHE1_2.
+      assumption.
+    - apply IHE1. assumption.
+    - rewrite H in H5. discriminate.
+    - rewrite H in H5. discriminate.
+    - apply IHE1. assumption.
+    - reflexivity.
+    - rewrite H in H2. discriminate.
+    - rewrite H in H4. discriminate.
+    - rewrite (IHE1_1 st'0 H3) in *.
+      apply IHE1_2. assumption. Qed.
+
+  Definition plus2 : com :=
+    <{ X := X + 2 }>.
+
+  Theorem plus2_spec : forall st n st',
+      st X = n ->
+      st =[ plus2 ]=> st' ->
+      st' X = n + 2.
+  Proof.
+    intros st n st' HX Heval.
+    inversion Heval.
+    subst. clear Heval. simpl.
+    apply t_update_eq.
+  Qed.
+
+  Definition XtimesYinZ : com :=
+    <{ Z := X * Y }>.
+
+  Theorem XtimesYinZ_spec : forall st n m st',
+      st X = n ->
+      st Y = m ->
+      st =[ XtimesYinZ ]=> st' ->
+      st' Z = n * m.
+  Proof.
+    intros st n m st' HX HY Heval.
+    inversion Heval.
+    subst.
+    simpl.
+    apply t_update_eq.
+  Qed.
+
+  Definition loop : com :=
+    <{ while true do
+         skip
+       end }>.
+
+  Theorem loop_never_stops : forall st st',
+      ~(st =[ loop ]=> st').
+  Proof.
+    intros st st' contra.
+    unfold loop in contra.
+    remember <{ while true do skip end }> as loopdef eqn:Heqloopdef.
+    induction contra ; try discriminate.
+    - inversion Heqloopdef; subst.
+      simpl in H.
+      discriminate.
+    - inversion Heqloopdef; subst.
+      apply IHcontra2.
+      reflexivity.
+  Qed.
+
+  Fixpoint no_whiles (c : com) : bool :=
+    match c with
+    | <{ skip }> => true
+    | <{ _ := _ }> => true
+    | <{ c1 ; c2 }> =>
+        andb (no_whiles c1) (no_whiles c2)
+    | <{ if _ then ct else cf end }> =>
+        andb (no_whiles ct) (no_whiles cf)
+    | <{ while _ do _ end }> => false
+    end.
+
+  Inductive no_whilesR : com -> Prop :=
+  | no_whilesSkip : no_whilesR <{ skip }>
+  | no_whilesAsgn (x : string) (a : aexp) : no_whilesR <{ x := a }>
+  | no_whilesSeq (c1 c2 : com) (H1 : no_whilesR c1) (H2 : no_whilesR c2) :
+    no_whilesR <{ c1 ; c2 }>
+  | no_whilesIf (b : bexp) (ct cf : com) (H1 : no_whilesR ct) (H2 : no_whilesR cf) :
+    no_whilesR <{ if b then ct else cf end }>.
+
+  Theorem no_whiles_eqv:
+    forall c, no_whiles c = true <-> no_whilesR c.
+  Proof.
+    intros c.
+    split.
+    - intros H.
+      induction c;
+        try (constructor ; reflexivity) ;
+        try (constructor ;
+             [ apply IHc1 ; reflexivity
+             | apply IHc2 ; reflexivity ]) ;
+        try (constructor ; [ apply IHc1 | apply IHc2 ] ;
+             inversion H;
+             apply andb_true_iff
+               with (b1 := no_whiles c1)
+                    (b2 := no_whiles c2)
+               in H1 as [G1 G2];
+             rewrite G1;
+             rewrite G2;
+             reflexivity).
+      + simpl in H. discriminate.
+    - intros H.
+      induction H;
+        try reflexivity;
+        try (simpl; rewrite IHno_whilesR1;
+             rewrite IHno_whilesR2; reflexivity).
+  Qed.
+
+  Theorem no_whiles_terminating : forall (st : state) (c : com),
+      no_whilesR c -> exists (st' : state),
+        st =[ c ]=> st'.
+  Proof.
+    intros st c H.
+    generalize dependent st.
+    induction c.
+    - intros.
+      exists st.
+      constructor.
+    - intros.
+      exists (x !-> (aeval st a) ; st).
+      constructor.
+      reflexivity.
+    - intros.
+      inversion H.
+      subst.
+      apply IHc1 with (st := st) in H0.
+      destruct H0 as [st' H1].
+      apply IHc2 with (st := st') in H3.
+      destruct H3 as [st'' H2].
+      exists st''.
+      apply (E_Seq c1 c2 st st' st'' H1 H2).
+    - intros.
+      inversion H.
+      subst.
+      destruct (beval st b) eqn:Eb ;
+        [ apply IHc1 with (st := st) in H0 as G
+        | apply IHc2 with (st := st) in H4 as G] ;
+        destruct G as [st' G1] ;
+        exists st' ;
+        constructor ;
+        assumption.
+    - intros.
+      inversion H.
+  Qed.
+
+
+  Inductive sinstr : Type :=
+  | SPush (n : nat)
+  | SLoad (x : string)
+  | SPlus
+  | SMinus
+  | SMult.
+
+  Fixpoint s_execute (st : state) (stack : list nat)
+    (prog : list sinstr)
+    : list nat :=
+    match prog with
+    | [] => stack
+    | (SPush n :: rest) => s_execute st (n :: stack) rest
+    | (SLoad x :: rest) => s_execute st (st x :: stack) rest
+    | (SPlus :: rest) => match stack with
+                         | x :: y :: ss =>
+                             s_execute st ((y + x) :: ss) rest
+                         | _ => s_execute st stack rest
+                         end
+    | (SMinus :: rest) => match stack with
+                          | x :: y :: ss =>
+                              s_execute st ((y - x) :: ss) rest
+                          | _ => s_execute st stack rest
+                          end
+    | (SMult :: rest) => match stack with
+                         | x :: y :: ss =>
+                             s_execute st ((y * x) :: ss) rest
+                         | _ => s_execute st stack rest
+                         end
+    end.
+
+  Example s_execute1 :
+    s_execute empty_st []
+      [SPush 5; SPush 3; SPush 1; SMinus]
+    = [2; 5].
+  Proof. reflexivity. Qed.
+
+  Fixpoint s_compile (e : aexp) : list sinstr :=
+    match e with
+    | ANum n => [SPush n]
+    | AId x => [SLoad x]
+    | APlus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SPlus]
+    | AMinus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMinus]
+    | AMult a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMult]
+    end.
+
+  Example s_compile1 :
+    s_compile <{ X - (2 * Y) }>
+      = [SLoad X; SPush 2; SLoad Y; SMult; SMinus].
+  Proof. reflexivity.
+  Qed.
+
+  Theorem execute_app : forall st p1 p2 stack,
+      s_execute st stack (p1 ++ p2) = s_execute st (s_execute st stack p1) p2.
+  Proof.
+    intros st p1 p2.
+    induction p1.
+    - intros.
+      reflexivity.
+    - intros.
+      destruct a eqn:Ea.
+      + simpl. apply (IHp1 (n :: stack)).
+      + simpl. apply (IHp1 (st x :: stack)).
+      + simpl. destruct stack.
+        { apply IHp1. }
+        destruct stack.
+        { apply IHp1. }
diff --git a/ImpParser.v b/ImpParser.v
new file mode 100644
index 0000000..9063b07
--- /dev/null
+++ b/ImpParser.v
@@ -0,0 +1,160 @@
+From Coq Require Import Strings.String.
+From Coq Require Import Strings.Ascii.
+From Coq Require Import Arith.Arith.
+From Coq Require Import Init.Nat.
+From Coq Require Import Arith.EqNat.
+From Coq Require Import Lists.List. Import ListNotations.
+From LF Require Import Maps Imp.
+
+Definition isWhite (c : ascii) : bool :=
+  let n := nat_of_ascii c in
+  orb (orb (n =? 32)
+         (n =? 9))
+    (orb (n =? 10)
+       (n =? 13)).
+
+Notation "x '<=?' y" := (x <=? y)
+                          (at level 70, no associativity) : nat_scope.
+
+Definition isLowerAlpha (c : ascii) : bool :=
+  let n := nat_of_ascii c in
+  andb (97 <=? n) (n <=? 122).
+
+Definition isAlpha (c : ascii) : bool :=
+  let n := nat_of_ascii c in
+  orb (andb (65 <=? n) (n <=? 90))
+    (andb (97 <=? n) (n <=? 122)).
+
+Definition isDigit (c : ascii) : bool :=
+  let n := nat_of_ascii c in
+  andb (48 <=? n) (n <=? 57).
+
+Inductive chartype := white | alpha | digit | other.
+
+Definition classifyChar (c : ascii) : chartype :=
+  if isWhite c then
+    white
+  else if isAlpha c then
+         alpha
+       else if isDigit c then
+              digit
+            else
+              other.
+
+Fixpoint list_of_string (s : string) : list ascii :=
+  match s with
+  | EmptyString => []
+  | String c s => c :: (list_of_string s)
+  end.
+
+Definition string_of_list (xs : list ascii) : string :=
+  fold_right String EmptyString xs.
+
+Definition token := string.
+
+Fixpoint tokenize_helper (cls : chartype) (acc xs : list ascii)
+  : list (list ascii) :=
+  let tk := match acc with
+            | [] => []
+            | _::_ => [rev acc]
+            end
+  in
+  match xs with
+  | [] => tk
+  | (x :: xs') =>
+      match cls, classifyChar x, x with
+      | _, _, "(" =>
+          tk ++ ["("] :: (tokenize_helper other [] xs')
+      | _, _, ")" =>
+          tk ++ [")"] :: (tokenize_helper other [] xs')
+      | _, white, _ =>
+          tk ++ (tokenize_helper white [] xs')
+      | alpha, alpha, x =>
+          tokenize_helper alpha (x :: acc) xs'
+      | digit, digit, x =>
+          tokenize_helper digit (x :: acc) xs'
+      | other, other, x =>
+          tokenize_helper other (x :: acc) xs'
+      | _, tp, x =>
+          tk ++ (tokenize_helper tp [x] xs')
+      end
+  end %char.
+
+Definition tokenize (s : string) : list string :=
+  map string_of_list (tokenize_helper white [] (list_of_string s)).
+
+Example tokenize_ex1 :
+  tokenize "abc12=3 223*(3+(a+c))" %string
+  = ["abc"; "12"; "="; "3"; "223";
+     "*"; "("; "3"; "+"; "(";
+     "a"; "+"; "c"; ")"; ")"]%string.
+Proof.
+  reflexivity.
+Qed.
+
+Inductive optionE (X : Type) : Type :=
+| SomeE (x : X)
+| NoneE (s : string).
+
+Arguments SomeE {X}.
+Arguments NoneE {X}.
+
+Notation "' p <- e1 ;; e2"
+  := (match e1 with
+      | SomeE p => e2
+      | NoneE err => NoneE err
+      end)
+       (right associativity, p pattern, at level 60, e1 at next level).
+
+Notation "'TRY' e1 'OR' e2"
+  := (
+    let result := e1 in
+    match result with
+    | SomeE _ => result
+    | NoneE _ => e2
+    end)
+       (right associativity,
+         at level 60, e1 at next level, e2 at next level).
+
+Open Scope string_scope.
+
+Definition parser (T : Type) :=
+  list token -> optionE (T * list token).
+
+Fixpoint many_helper {T} (p : parser T) acc steps xs :=
+  match steps, p xs with
+  | 0, _ =>
+      NoneE "Too many recursive calls"
+  | _, NoneE _ =>
+      SomeE ((rev acc), xs)
+  | S steps', SomeE (t, xs') =>
+      many_helper p (t :: acc) steps' xs'
+  end.
+
+Definition many {T} (p : parser T) (steps : nat) : parser (list T) :=
+  many_helper p [] steps.
+
+Definition firstExpect {T} (t : token) (p : parser T)
+  : parser T :=
+  fun xs => match xs with
+            | x :: xs' =>
+                if string_dec x t
+                then p xs'
+                else NoneE ("expected '" ++ t ++ "'.")
+            | [] =>
+                NoneE ("expected '" ++ t ++ "'.")
+            end.
+
+Definition expect (t : token) : parser unit :=
+  firstExpect t (fun xs => SomeE (tt, xs)).
+
+Definition parseIdentifier (xs : list token)
+  : optionE (string * list token) :=
+  match xs with
+  | [] => NoneE "Expected identifier"
+  | x :: xs' =>
+      if forallb isLowerAlpha (list_of_string x) then
+        SomeE (x, xs')
+      else
+        NoneE ("Illegal identifier:'" ++ x ++ "'")
+  end.
diff --git a/IndPrinciples.v b/IndPrinciples.v
new file mode 100644
index 0000000..671e960
--- /dev/null
+++ b/IndPrinciples.v
@@ -0,0 +1,139 @@
+From Coq Require Import Arith.Arith.
+From Coq Require Import Bool.Bool.
+From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import Lists.List.
+From Coq Require Import Strings.String.
+Import ListNotations.
+Set Default Goal Selector "!".
+
+Theorem mul_0_r' : forall n : nat,
+    n * 0 = 0.
+Proof.
+  apply nat_ind.
+  - reflexivity.
+  - simpl.
+    intros.
+    apply H.
+Qed.
+
+Inductive rgb : Type :=
+| red
+| green
+| blue.
+
+(* rgb_ind :
+   forall P : rgb -> Prop,
+          P red ->
+          P green ->
+          P blue ->
+          forall color : rgb, P color
+*)
+
+Check rgb_ind.
+
+Inductive booltree : Type :=
+| bt_empty
+| bt_leaf (b : bool)
+| bt_branch (b : bool) (t1 t2 : booltree).
+
+Definition base_case (P : booltree -> Prop) : Prop :=
+  P bt_empty.
+
+Definition leaf_case (P : booltree -> Prop) : Prop :=
+  forall (b : bool), P (bt_leaf b).
+
+Definition branch_case (P : booltree -> Prop) : Prop :=
+  forall (b : bool) (t1 : booltree),
+    P t1 -> forall (t2 : booltree),
+    P t2 -> P (bt_branch b t1 t2).
+
+Definition booltree_ind_type :=
+  forall (P : booltree -> Prop),
+    base_case P ->
+    leaf_case P ->
+    branch_case P ->
+    forall (b : booltree), P b.
+
+Theorem booltree_ind_type_correct : booltree_ind_type.
+Proof.
+  exact booltree_ind.
+Qed.
+
+Inductive Toy :=
+| con1 (b : bool)
+| con2 (n : nat) (t : Toy).
+
+Theorem Toy_correct : exists f g,
+  forall P : Toy -> Prop,
+    (forall b : bool, P (f b)) ->
+    (forall (n : nat) (t : Toy), P t -> P (g n t)) ->
+    forall t : Toy, P t.
+Proof.
+  exists con1, con2.
+  exact Toy_ind.
+Qed.
+
+Fixpoint build_proof
+  (P : nat -> Prop)
+  (evPO : P 0)
+  (evPS : forall n : nat, P n -> P (S n))
+  (n : nat) : P n :=
+  match n with
+  | 0 => evPO
+  | S k => evPS k (build_proof P evPO evPS k)
+  end.
+
+Definition nat_ind2 :
+  forall (P : nat -> Prop),
+    P 0 ->
+    P 1 ->
+    (forall n : nat, P n -> P (S (S n))) ->
+    forall n : nat, P n :=
+  fun P P0 P1 PSS =>
+    fix f (n : nat) := match n with
+                       | 0 => P0
+                       | 1 => P1
+                       | S (S n') => PSS n' (f n')
+                       end.
+
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Inductive t_tree (X : Type) : Type :=
+| t_leaf
+| t_branch : (t_tree X * X * t_tree X) -> t_tree X.
+
+Arguments t_leaf {X}.
+Arguments t_branch {X}.
+
+Fixpoint reflect {X : Type} (t : t_tree X) : t_tree X :=
+  match t with
+  | t_leaf => t_leaf
+  | t_branch (l, v, r) => t_branch (reflect r, v, reflect l)
+  end.
+
+Definition better_t_tree_ind_type : Prop :=
+  forall (X: Type) (P : t_tree X -> Prop),
+    P t_leaf ->
+    (forall (l r : t_tree X) (v : X),
+      P l -> P r -> P (t_branch (l, v, r))) ->
+      forall (t : t_tree X), P t.
+
+Definition better_t_tree_ind : better_t_tree_ind_type :=
+  fun X P Pl Pb =>
+    fix f t := match t with
+               | t_leaf => Pl
+               | t_branch (l, v, r) => Pb l r v (f l) (f r)
+               end.
+
+Theorem reflect_involution : forall (X : Type) (t : t_tree X),
+    reflect (reflect t) = t.
+Proof.
+  intros X.
+  apply better_t_tree_ind.
+  - reflexivity.
+  - intros l r v Hl Hr.
+    simpl.
+    rewrite Hl.
+    rewrite Hr.
+    reflexivity.
+Qed.
diff --git a/Indprop.v b/Indprop.v
index c80c062..3fc3564 100644
--- a/Indprop.v
+++ b/Indprop.v
@@ -316,8 +316,9 @@ Module Playground.
     inversion H2.
   Qed.
 
-  Definition lt (n m : nat) := lt (S n) m.
-  Notation "n < m" := (lt n m).
+    Definition lt (n m : nat) := lt (S n) m.
+    Notation "n < m" := (lt n m).
+
 End Playground.
 
 Inductive total_relation : nat -> nat -> Prop :=
@@ -1390,29 +1391,128 @@ Proof.
     reflexivity.
 Qed.
 
-Theorem length_ind : forall {X: Type} (P : list X -> Prop),
-    P [] ->
-    (forall (l1 : list X), (forall (l2 : list X), S (length l2) <= length l1 -> P l2) -> P l1) ->
-    forall (l : list X), P l.
-Proof.    
-  intros X P H1 H2 l.
-  assert (G: forall l', S (length l') <= length l -> P l').
-  - induction l' as [ | h' t' IHt'].
-    + intros G.
-      apply H1.
-    + intros G.
-      simpl in *.
-      apply H2.
+Inductive NotIn {X: Type}: X -> list X -> Prop :=
+| empty_notin (x: X): NotIn x []
+| cons_notin (x: X) (x': X) (l: list X) (E1: x <> x') (E2: NotIn x l): NotIn x (x' :: l).
 
-  
-      
-      
-Theorem palindrome_converse : forall {X : Type} (l: list X),
-    l = rev l -> pal l.
+Inductive NoDup {X: Type}: list X -> Prop :=
+| empty_nodup: NoDup []
+| cons_nodup (x: X) (l: list X) (E: NoDup l) (pf: NotIn x l): NoDup (x :: l).
+
+Inductive disjoint {X: Type}: list X -> list X -> Prop :=
+| empty_disjoint l2 : disjoint [] l2
+| cons_disjoint (x: X) (l1 l2: list X) (E1: disjoint l1 l2) (E2: NotIn x l2): disjoint (x :: l1) l2.
+
+Example disjoint_ex1: disjoint [1; 2; 3] [4; 5; 6].
 Proof.
-  intros X.
-  destruct l as [ | h t].
-  - intros H. apply pal_empty.
+  apply cons_disjoint.
+  - apply cons_disjoint.
+    + apply cons_disjoint.
+      * apply empty_disjoint.
+      * apply cons_notin.
+        { trivial. }
+        apply cons_notin.
+        { intros H. discriminate H. }
+        apply cons_notin.
+        { discriminate. }
+        apply empty_notin.
+    + apply cons_notin.
+      { discriminate. }
+      apply cons_notin.
+      { discriminate. }
+      apply cons_notin.
+      discriminate.
+      apply empty_notin.
+  - apply cons_notin.
+    { discriminate. }
+    apply cons_notin.
+    { discriminate. }
+    apply cons_notin.
+    { discriminate. }
+    apply empty_notin.
+Qed.
+
+Lemma in_split : forall (X: Type) (x: X) (l: list X),
+    In x l ->
+    exists l1 l2, l = l1 ++ x :: l2.
+Proof.
+  intros X x.
+  induction l as [ | h t IHt].
   - intros H.
     simpl in H.
-    
+    exfalso.
+    apply H.
+  - intros H.
+    destruct H as [H1 | H2].
+    + exists [], t.
+      simpl.
+      rewrite H1.
+      reflexivity.
+    + apply IHt in H2.
+      destruct H2 as [l1' [l2' H2]].
+      exists (h :: l1'), l2'.
+      rewrite H2.
+      reflexivity.
+Qed.
+
+Inductive repeats {X: Type} : list X -> Prop :=
+| repeats_cons (x: X) (l: list X) (E: In x l): repeats (x :: l)
+| repeats_non (x: X) (l: list X) (E: repeats l): repeats (x :: l).
+
+Require Import Arith.
+
+Theorem pigeonhole_principle:
+  excluded_middle -> forall (X: Type) (l1 l2: list X),
+      (forall x, In x l1 -> In x l2) ->
+      length l2 < length l1 ->
+      repeats l1.
+Proof.
+  intros EM X l1. induction l1 as [ | h t IHt].
+  - simpl. intros. inversion H0.
+  - intros l2 H1 H2.
+    destruct (EM (In h t)) as [G | G].
+    + apply repeats_cons.
+      apply G.
+    + destruct l2 as [ | h2 t2].
+      * simpl in H1.
+        exfalso.
+        apply H1 with (x := h).
+        left.
+        reflexivity.
+      * destruct (in_split _ h (h2::t2)) as [la [lb E]].
+        -- apply (H1 h).
+           simpl.
+           left.
+           reflexivity.
+        -- apply repeats_non.
+           apply (IHt (la ++ lb)).
+           ++ intros x G'.
+              rewrite E in H1.
+              assert (Neq : h <> x).
+              { intros contra.
+                rewrite contra in G.
+                apply G.
+                apply G'. }
+              assert (In_split_Neq : In x (la ++ h :: lb) -> In x (la ++ lb)).
+              { intros H'.
+                apply In_app_iff.
+                apply In_app_iff in H'.
+                destruct H' as [H' | H'].
+                - left. apply H'.
+                - right. simpl in H'. destruct H' as [H' | H'].
+                  + exfalso. apply Neq. apply H'.
+                  + apply H'.
+              } 
+              apply In_split_Neq.
+              apply H1.
+              simpl.
+              right.
+              apply G'.
+           ++ rewrite E in H2.
+              rewrite app_length in H2.
+              simpl in H2.
+              rewrite <- plus_n_Sm in H2.
+              rewrite app_length.
+              apply PeanoNat.lt_S_n.
+              apply H2.
+Qed.
diff --git a/Makefile b/Makefile
index ab8ad86..fee8969 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.18.0
+## GNUMakefile for Coq 8.19.1
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -45,7 +45,7 @@ HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
 OCAMLWARN         := $(COQMF_WARN)
 
 Makefile.conf: _CoqProject
-	coq_makefile -f _CoqProject Basics.v Induction.v Lists.v Logic.v Polymorphism.v Tactics.v -o Makefile
+	coq_makefile -f _CoqProject Maps.v Imp.v -o Makefile
 
 # This file can be created by the user to hook into double colon rules or
 # add any other Makefile code he may need
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.18.0
+COQMAKEFILE_VERSION:=8.19.1
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -307,6 +307,14 @@ else
   TIMING_ARG=
 endif
 
+ifneq (,$(PROFILING))
+  PROFILE_ARG=-profile $<.prof.json
+  PROFILE_ZIP=gzip $<.prof.json
+else
+  PROFILE_ARG=
+  PROFILE_ZIP=true
+endif
+
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -758,9 +766,9 @@ $(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
 
 
 $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
-	$(SHOW)'CAMLOPT -shared -g -o $@'
+	$(SHOW)'CAMLOPT -shared -o $@'
 	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
-		-shared -g -o $@ $<
+		-shared -o $@ $<
 
 $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
 	$(SHOW)'CAMLC -a -o $@'
@@ -772,9 +780,9 @@ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
 
 
 $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
-	$(SHOW)'CAMLOPT -shared -g -o $@'
+	$(SHOW)'CAMLOPT -shared -o $@'
 	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
-		-shared -g -o $@ $<
+		-shared -o $@ $<
 
 $(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack
 	$(SHOW)'CAMLOPT -a -o $@'
@@ -794,9 +802,9 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 
 # This rule is for _CoqProject with no .mllib nor .mlpack
 $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
-	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -g -o $@'
+	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
 	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
-		-shared -g -o $@ $<
+		-shared -o $@ $<
 
 # can't make
 # https://www.gnu.org/software/make/manual/make.html#Static-Pattern
@@ -808,12 +816,13 @@ ifneq (,$(filter grouped-target,$(.FEATURES)))
 define globvorule=
 
 # take care to $$ variables using $< etc
-  $(1).vo $(1).glob &: $(1).v | $(VDFILE)
-	$(SHOW)COQC $(1).v
-	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v
+  $(1).vo $(1).glob &: $(1).v | $$(VDFILE)
+	$$(SHOW)COQC $(1).v
+	$$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v
+	$$(HIDE)$$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
-	$(SHOW)COQNATIVE $(1).vo
-	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
+	$$(SHOW)COQNATIVE $(1).vo
+	$$(HIDE)$$(call TIMER,$(1).vo.native) $$(COQNATIVE) $$(COQLIBS) $(1).vo
 endif
 
 endef
@@ -821,7 +830,8 @@ else
 
 $(VOFILES): %.vo: %.v | $(VDFILE)
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
 	$(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@
diff --git a/Makefile.conf b/Makefile.conf
index be67555..f05655d 100644
--- a/Makefile.conf
+++ b/Makefile.conf
@@ -1,5 +1,5 @@
 # This configuration file was generated by running:
-# coq_makefile -f _CoqProject Basics.v Induction.v Lists.v Logic.v Polymorphism.v Tactics.v -o Makefile
+# coq_makefile -f _CoqProject Maps.v Imp.v -o Makefile
 
 COQBIN?=
 ifneq (,$(COQBIN))
@@ -14,7 +14,7 @@ COQMKFILE ?= "$(COQBIN)coq_makefile"
 #                                                                             #
 ###############################################################################
 
-COQMF_CMDLINE_VFILES := Basics.v Induction.v Lists.v Logic.v Polymorphism.v Tactics.v
+COQMF_CMDLINE_VFILES := Maps.v Imp.v
 COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
 COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
 COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
@@ -42,9 +42,9 @@ COQMF_CMDLINE_COQLIBS =
 #                                                                             #
 ###############################################################################
 
-COQMF_COQLIB=/usr/lib64/ocaml/coq/
-COQMF_COQCORELIB=/usr/lib64/ocaml/coq/../coq-core/
-COQMF_DOCDIR=/usr/share/doc/coq/
+COQMF_COQLIB=/usr/lib/coq/
+COQMF_COQCORELIB=/usr/lib/coq/../coq-core/
+COQMF_DOCDIR=/usr/share/doc/
 COQMF_OCAMLFIND=/usr/bin/ocamlfind
 COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
 COQMF_WARN=-warn-error +a-3
diff --git a/Maps.v b/Maps.v
new file mode 100644
index 0000000..46f7c07
--- /dev/null
+++ b/Maps.v
@@ -0,0 +1,255 @@
+From Coq Require Import Arith.Arith.
+From Coq Require Import Bool.Bool.
+From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import Lists.List.
+From Coq Require Import Strings.String.
+Import ListNotations.
+Set Default Goal Selector "!".
+
+Definition total_map (A : Type) := string -> A.
+
+Definition t_empty {A : Type} (v : A) : total_map A :=
+  (fun _ => v).
+
+Definition t_update {A : Type} (m : total_map A)
+  (x : string) (v : A) :=
+  fun x' => if String.eqb x x' then v else m x'.
+
+Definition examplemap :=
+  t_update (t_update (t_empty false) "foo" true) "bar" true.
+
+Notation "'_' '!->' v" := (t_empty v) (at level 100, right associativity).
+
+Example example_empty := (_ !-> false).
+
+Notation "x '!->' v ';' m" := (t_update m x v)
+                                (at level 100, v at next level, right associativity).
+
+Definition examplemap' :=
+  ( "bar" !-> true;
+    "foo" !-> true;
+    _ !-> false
+  ).
+
+Lemma t_apply_empty : forall (A : Type) (x : string) (v : A),
+    (_ !-> v) x = v.
+Proof.
+  intros A x v.
+  reflexivity.
+Qed.
+
+Lemma t_update_eq : forall (A : Type) (m : total_map A) x v,
+    (x !-> v ; m) x = v.
+Proof.
+  intros A m x v.
+  unfold t_update.
+  rewrite String.eqb_refl.
+  reflexivity.
+Qed.
+
+Theorem t_update_neq : forall (A : Type) (m : total_map A) x1 x2 v,
+    x1 <> x2 ->
+    (x1 !-> v ; m) x2 = m x2.
+Proof.
+  intros A m x1 x2 v H.
+  unfold t_update.
+  rewrite <- String.eqb_neq in H.
+  rewrite H.
+  reflexivity.
+Qed.
+
+Lemma t_update_shadow : forall (A : Type) (m : total_map A) x v1 v2,
+    (x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m).
+Proof.
+  intros A m x v1 v2.
+  unfold t_update.
+  apply functional_extensionality_dep.
+  intros x'.
+  destruct (x =? x')%string ; reflexivity.
+Qed.
+
+Theorem t_update_same : forall (A : Type) (m : total_map A) x,
+    (x !-> m x ; m) = m.
+Proof.
+  intros A m x.
+  apply functional_extensionality.
+  intros x'.
+  destruct (eqb_spec x x').
+  - rewrite e.
+    unfold t_update.
+    rewrite eqb_refl.
+    reflexivity.
+  - unfold t_update.
+    apply eqb_neq in n.
+    rewrite n.
+    reflexivity.
+Qed.
+
+Theorem t_update_permute : forall (A : Type) (m : total_map A)
+                                  v1 v2 x1 x2,
+    x2 <> x1 ->
+    (x1 !-> v1 ; x2 !-> v2 ; m)
+    =
+      (x2 !-> v2 ; x1 !-> v1 ; m).
+Proof.
+  intros A m v1 v2 x1 x2 H.
+  apply functional_extensionality.
+  intros x.
+  destruct (eqb_spec x x1).
+  - unfold t_update.
+    rewrite e.
+    rewrite eqb_refl.
+    rewrite (proj2 (eqb_neq x2 x1) H).
+    reflexivity.
+  - unfold t_update.
+    rewrite eqb_sym.
+    rewrite (proj2 (eqb_neq x x1) n).
+    reflexivity.
+Qed.
+
+Definition partial_map (A : Type) := total_map (option A).
+
+Definition empty {A : Type} : partial_map A :=
+  t_empty None.
+
+Definition update {A : Type} (m : partial_map A)
+  (x : string) (v : A) :=
+  (x !-> Some v ; m).
+
+Notation "x '|->' v ';' m" := (update m x v)
+                                (at level 100, v at next level, right associativity).
+
+Notation "x '|->' v" := (update empty x v)
+                          (at level 100).
+
+Definition examplepmap :=
+  ("Church" |-> true ; "Turing" |-> false).
+
+Lemma apply_empty : forall (A : Type) (x : string),
+    @empty A x = None.
+Proof.
+  intros.
+  unfold empty.
+  rewrite t_apply_empty.
+  reflexivity.
+Qed.
+
+Lemma update_eq : forall (A : Type) (m : partial_map A) x v,
+    (x |-> v ; m) x = Some v.
+Proof.
+  intros.
+  unfold update.
+  rewrite t_update_eq.
+  reflexivity.
+Qed.
+
+#[global] Hint Resolve update_eq : core.
+
+Theorem update_neq : forall (A : Type) (m : partial_map A) x1 x2 v,
+    x2 <> x1 ->
+    (x2 |-> v ; m) x1 = m x1.
+Proof.
+  intros A m x1 x2 v H.
+  unfold update.
+  rewrite t_update_neq.
+  - reflexivity.
+  - apply H.
+Qed.
+
+Lemma update_shadow : forall (A : Type) (m : partial_map A) x v1 v2,
+    (x |-> v2 ; x |-> v1 ; m) = (x |-> v2 ; m).
+Proof.
+  intros.
+  unfold update.
+  rewrite t_update_shadow.
+  reflexivity.
+Qed.
+
+Theorem update_same : forall (A : Type) (m : partial_map A) x v,
+    m x = Some v ->
+    (x |-> v ; m) = m.
+Proof.
+  intros.
+  unfold update.
+  rewrite <- H.
+  apply t_update_same.
+Qed.
+
+Theorem update_permute : forall (A : Type) (m : partial_map A)
+                                x1 x2 v1 v2,
+    x2 <> x1 ->
+    (x1 |-> v1 ; x2 |-> v2 ; m) = (x2 |-> v2 ; x1 |-> v1 ; m).
+  intros A m x1 x2 v1 v2.
+  unfold update.
+  apply t_update_permute.
+Qed.
+
+Definition includedin {A : Type} (m m' : partial_map A) :=
+  forall x v, m x = Some v -> m' x = Some v.
+
+Lemma includedin_update : forall (A : Type) (m m' : partial_map A)
+                                 (x : string) (vx : A),
+    includedin m m' ->
+    includedin (x |-> vx ; m) (x |-> vx ; m').
+Proof.
+  unfold includedin.
+  intros A m m' x vx H.
+  intros y vy.
+  destruct (eqb_spec x y) as [Hxy | Hxy].
+  - rewrite Hxy.
+    rewrite update_eq.
+    rewrite update_eq.
+    intro H1 ; apply H1.
+  - rewrite update_neq.
+    + rewrite update_neq.
+      * apply H.
+      * apply Hxy.
+    + apply Hxy.
+Qed.
+
+Definition propositional_extensionality : Prop :=
+  forall (P Q : Prop), (P <-> Q) -> P = Q.
+
+Theorem pe_implies_or_eq :
+  propositional_extensionality ->
+  forall (P Q : Prop), (P \/ Q) = (Q \/ P).
+Proof.
+  intros.
+  apply H.
+  split.
+  - intros [HP | HQ].
+    + right. apply HP.
+    + left. apply HQ.
+  - intros [HQ | HP].
+    + right. apply HQ.
+    + left. apply HP.
+Qed.
+
+Lemma pe_implies_true_eq :
+  propositional_extensionality ->
+  forall (P : Prop), P -> True = P.
+Proof.
+  intros PE P H.
+  apply PE.
+  split.
+  - intros _.
+    apply H.
+  - intros _.
+    apply I.
+Qed.
+
+Definition proof_irrelevance : Prop :=
+  forall (P : Prop) (pf1 pf2 : P), pf1 = pf2.
+
+Theorem pe_implies_pi :
+  propositional_extensionality -> proof_irrelevance.
+Proof.
+  intros PE P pf1 pf2.
+  apply (pe_implies_true_eq PE) in pf1 as H. 
+  revert pf1 pf2.
+  rewrite <- H.
+  intros pf1 pf2.
+  destruct pf1.
+  destruct pf2.
+  reflexivity.
+Qed.
diff --git a/Rel.v b/Rel.v
new file mode 100644
index 0000000..a40472b
--- /dev/null
+++ b/Rel.v
@@ -0,0 +1,76 @@
+From Coq Require Import Arith.Arith.
+From Coq Require Import Bool.Bool.
+From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import Lists.List.
+From Coq Require Import Strings.String.
+Import ListNotations.
+Set Default Goal Selector "!".
+
+Definition relation (X: Type) := X -> X -> Prop.
+
+Definition partial_function {X: Type} (R: relation X) :=
+  forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
+
+Inductive next_nat : nat -> nat -> Prop :=
+| nn n : next_nat n (S n).
+
+Check next_nat : relation nat.
+
+Theorem next_nat_partial_function: partial_function next_nat.
+Proof.
+  unfold partial_function.
+  intros x y1 y2 H1 H2.
+  inversion H1.
+  inversion H2.
+  reflexivity.
+Qed.
+
+Theorem le_not_a_partial_function :
+  ~ (partial_function le).
+Proof.
+  unfold not.
+  unfold partial_function.
+  intros Hc.
+  assert (0 = 1) as Nonsense. { 
+    apply Hc with (x := 0).
+    - apply le_n.
+    - apply le_S. apply le_n.
+  }
+  discriminate Nonsense.
+Qed.
+
+Inductive total_relation : nat -> nat -> Prop :=
+| rel_0 (n : nat) : total_relation 0 n
+| rel_Sn_m (n m : nat) (H : total_relation n m) : total_relation (S n) m.
+
+Theorem total_relation_not_partial_function :
+  ~ (partial_function total_relation).
+Proof.
+  unfold partial_function.
+  intros Hc.
+  assert (0 = 1) as Nonsense. {
+    apply Hc with (x := 1) ; apply rel_Sn_m ; apply rel_0.
+  }
+  discriminate.
+Qed.
+
+Inductive empty_relation : nat -> nat -> Prop :=
+| rel_contra (n m : nat) (H : S n = 0) : empty_relation n m.
+
+Theorem empty_relation_partial_function :
+  partial_function empty_relation.
+Proof.
+  unfold partial_function.
+  intros x y1 y2 H1 H2.
+  exfalso.
+  inversion H1.
+  discriminate.
+Qed.
+
+Definition reflexive {X: Type} (R: relation X) :=
+  forall a: X, R a a.
+
+Theorem le_reflexive : reflexive le.
+Proof.
+  exact le_n.
+Qed.
diff --git a/Rel.v~ b/Rel.v~
new file mode 100644
index 0000000..32ea82d
--- /dev/null
+++ b/Rel.v~
@@ -0,0 +1,42 @@
+From Coq Require Import Arith.Arith.
+From Coq Require Import Bool.Bool.
+From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import Lists.List.
+From Coq Require Import Strings.String.
+Import ListNotations.
+Set Default Goal Selector "!".
+
+Definition relation (X: Type) := X -> X -> Prop.
+
+Definition partial_function {X: Type} (R: relation X) :=
+  forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
+
+Inductive next_nat : nat -> nat -> Prop :=
+| nn n : next_nat n (S n).
+
+Check next_nat : relation nat.
+
+Theorem next_nat_partial_function: partial_function next_nat.
+Proof.
+  unfold partial_function.
+  intros x y1 y2 H1 H2.
+  inversion H1.
+  inversion H2.
+  reflexivity.
+Qed.
+
+Theorem le_not_a_partial_function :
+  ~ (partial_function le).
+Proof.
+  unfold not.
+  unfold partial_function.
+  intros Hc.
+  assert (0 = 1) as Nonsense. { 
+    apply Hc with (x := 0).
+    - apply le_n.
+    - apply le_S. apply le_n.
+  }
+  discriminate Nonsense.
+Qed.
+
+Inductive total_relation : nat -> nat -> Prop :=