Require Import Arith.
Require Import List.

Check 0.
Check 1.
Check nat.

Check true.
Check bool.

Check Set.
Check Type.

Check ((fun (n: nat) => n + 1) (7 + 2)).
(* Print (((fun (n: nat) => n + 1) (7 + 2))). *)

Check True.
Check Prop.
Check (forall a b : Prop, a /\ b -> a).

Theorem zero: nat.
Proof.
  exact 0.
Save.

Theorem prop0: forall a b: Prop, a /\ b -> a.
Proof.
  intro. intro. intro. elim H. intros. exact H0.
Save.
Theorem prop1: forall a b: Prop, a /\ b -> a.
Proof.
  intros. elim H. intros. exact H0.
Save.
Theorem prop2: forall a b: Prop, a /\ b -> a.
Proof.
  tauto.
Save.
Check prop0.
Print prop0.

Theorem exo1_form_0: forall a b c : Prop, a /\ (b /\ c) -> (a /\ b) /\ c.
Proof.
  intros. elim H. intros. elim H1. intros.
  split.
    split; trivial.
    trivial.
Save.
Theorem exo1_form_1: forall a b c : Prop, a \/ (b \/ c) -> (c \/ a) \/ b.
Proof.
  intros.
  elim H; intros.
  left. right. exact H0.
  elim H0; intro.
  right. trivial.
  left. left. trivial.
Qed.
Theorem exo1_form_2: forall a : Prop, ~~~a -> ~a.
Proof.
  intros. intro. apply H. intro. exact (H1 H0).
Save.
Theorem exo1_form_3: forall a b: Prop, (a -> b) -> ~b -> ~a.
Proof.
  intros. intro. exact (H0 (H H1)).
Save.
Theorem exo1_form_4: forall a : Prop, ~~(a \/ ~a).
Proof.
  intros. intro. apply H. right. intro. apply H. left. trivial.
Save.
Print exo1_form_4. 
Theorem exo1_form_5: forall a b : Prop, ~~~a -> a -> b.
Proof.
  (*intros.*)
  (*exfalso. *)
  exact (fun (a b: Prop) => fun (H: ~~~a) => fun (H0: a) => False_ind b (exo1_form_2 a H H0)).
Save.

Inductive tree: Set :=
  | leaf : tree
  | node : tree -> tree -> tree.
Check tree_ind.

Print nat.
Check nat_ind.

Print and.
Check and_ind.
Print prop0.
Print or.
Check or_ind.
Print True.
Print False.
Check False_ind.

Print plus.
Print Nat.add.

Lemma plus_com_1: forall n : nat, S n = n + 1.
Proof.
  induction n.
  trivial.
  rewrite IHn at 1.
  trivial.
Save.
Print plus_com_1.

(*
Lemma plus_com: forall n m: nat, n + m = m + n.
Proof.
  induction n. simpl. trivial.
  simpl. induction m. simpl.
  induction n.
  trivial. trivial.
*)
Fixpoint sum_n (n: nat): nat :=
  match n with
    | O => O
    | S p => n + sum_n p
  end.
Lemma sum_n_form: forall n: nat, 2 * sum_n n = S n * n.
Proof.
  induction n.
  trivial.
  cutrewrite (2 * sum_n (S n) = 2 * S n + 2 * sum_n n).
  rewrite IHn.
  simpl.
  rewrite (plus_comm n 0). simpl.
  rewrite <- (plus_assoc n (S n) (n + n * n)). simpl.
  rewrite (mult_comm n (S n)). simpl. trivial.
  simpl.
  rewrite <- (plus_assoc n (sum_n n) 0).
  rewrite (plus_comm n 0).
  rewrite (plus_comm (sum_n n) 0).
  simpl.
  rewrite (plus_comm (n + sum_n n) (S (n + sum_n n))).
  simpl.
  rewrite <- (plus_assoc n (sum_n n) (n + sum_n n)).
  rewrite (plus_comm (sum_n n) (n + sum_n n)).
  rewrite <- (plus_assoc n (sum_n n) (sum_n n)).
  rewrite (plus_comm n (S n)).
  simpl.
  rewrite <- (plus_assoc n n (sum_n n + sum_n n)).
  trivial.
Qed.

Inductive expr : Set :=
  | e_cst: nat -> expr
  | e_add: expr -> expr -> expr
  | e_mul: expr -> expr -> expr
.
Fixpoint eval (e: expr): nat :=
  match e with
    | e_cst n => n
    | e_add e0 e1 => eval e0 + eval e1
    | e_mul e0 e1 => eval e0 * eval e1
  end.
Inductive inst : Set :=
  | i_push: nat -> inst
  | i_add:  inst
  | i_mul:  inst.
Definition code : Set := list inst.
Fixpoint compile (e: expr): code :=
  match e with
    | e_cst n => i_push n :: nil
    | e_add e0 e1 => (compile e0) ++ (compile e1) ++ (i_add :: nil)
    | e_mul e0 e1 => (compile e0) ++ (compile e1) ++ (i_mul :: nil)
  end.
Definition pile: Set := list nat.
Print option.
Fixpoint inst_eval (i: inst) (p: pile): option pile :=
  match i with
    | i_push n=>
      Some (n :: p)
    | i_add =>
      match p with
        | nil | _ :: nil => None
        | v0 :: v1 :: q => Some (v0 + v1 :: q)
      end
    | i_mul =>
      match p with
        | nil | _ :: nil => None
        | v0 :: v1 :: q => Some (v0 * v1 :: q)
      end
  end.