test.v

Inductive Nat :=
| Z : Nat
| S : Nat -> Nat.

Fixpoint plus (x : Nat) (y : Nat) : Nat :=
    match x with
    | Z => y
    | S x' => S (plus x' y)
    end.

Eval simpl in plus (S (S Z)) (S Z).

Lemma plus_z : forall n, plus Z n = n.
Proof.
   (* Goal on the bottom, hypothesis on the top *)
    intro n.
    simpl.
    reflexivity.
    (* reflexivity is a built in tactic, just roll with it? *)
Qed.

Print plus_z.
Check plus_z.


(* Easy, as we defined plus to match on the first argument. *)


Check Nat_ind.
(*
     Nat_ind : forall P : Nat -> Prop,
       P Z ->
       (forall n : Nat, P n -> P (S n)) ->
       forall n : Nat,
        P n
       *)
Check eq_ind_r.
(*
eq_ind_r
     : forall (A : Type)
     (x : A)
     (P : A -> Prop),
       P x ->
       forall y : A,
       y = x ->
       P y
*)

Module Type Sig.
End Sig.
Module Export Foo <: Sig.
Lemma plus_n_z : forall n, plus n Z = n.
Proof.
   (* Goal on the bottom, hypothesis on the top *)
    intro n.
    (* This is weaker than induction *)
    refine (Nat_ind (fun n => plus n Z = n) eq_refl _ _).
    intro n'.
    intro IH.
    simpl.
    refine (@eq_ind_r
                Nat (* A *)
                n' (* x *)
                (fun y: Nat => S y = S n' ) (* P *)
                eq_refl (* P x *)
                (* Px = S n' = S n' *)
                (plus n' Z) (* y *)
                IH (* P y *) ).
Qed.
    
    Hypothesis n : Nat.
    Theorem Foo': plus n (S Z) = S n.
    Proof.
        induction n.
        simpl.
        reflexivity.
        simpl.
        rewrite IHn0.
        reflexivity.
    Qed.
    Hint Resolve plus_n_z.
End Foo.

Goal  forall n, plus n Z = n.
apply plus_n_z.
Hint Resolve plus_n_z.
Qed.


Check Foo.
Definition plus_n_z' : forall n, plus n Z = n := (fun n : Nat =>
    Nat_ind (fun n => plus n Z = n) 
    (* zero case *) eq_refl
    (* inductive case *)
    (fun n' (IHn : plus n' Z = n') =>
        eq_ind_r (fun n : Nat => ) eq_refl IHn) n).                            

Inductive boolean := true | false.
Inductive True := tt.
Inductive False := .

Lemma false_is_awesome : False -> plus Z Z = S Z.
    intro x.
    destruct x.
Qed.


Theorem ClassTable_rect (CT: ctable) : forall P : cname -> Type,
    directed_ct CT ->
    Object \notin dom CT ->
    P Object ->
    (forall (C D : cname) fs ms,
      ok_type_ CT D ->
      binds C (D, fs, ms) CT ->
      P D -> P C) ->
    (forall C: cname, ok_type_ CT C -> P C).