(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                               demobastad.v                               *)
(****************************************************************************)

Section NewInductifs.

Inductive Bool : Set := true : Bool | false : Bool.
Inductive Nat : Set := O : Nat | S : Nat -> Nat.

Print Nat.
Print Nat_rec.

Scheme Nat_prim_rec := Minimality for Nat Sort Set.

Definition neg : Bool -> Bool := 
   [b:Bool]<Bool>Cases b of true => false | _ => true end.

Fixpoint plus [n,m:Nat] : Nat := 
   <Nat>Cases m of (S m1) => (plus n m1) | _ => O  end.

Fixpoint minus [n:Nat] : Nat -> Nat := 
    [m:Nat]<Nat>Cases n  m of 
                O _ => O  
           | (S n1) O => n 
           | (S n1) (S m1) => (minus n1 m1) 
           end.

Theorem minus_O_m : (m:Nat)(minus O m)=O.
Reflexivity.
Qed.

Theorem minus_Sn_O : (n:Nat)(minus (S n) O)=(S n).
Reflexivity.
Qed.

Theorem minus_Sn_Sm : (n,m:Nat)(minus (S n) (S m))=(minus n m).
Simpl.
Reflexivity.
Qed.

Fixpoint even [n:Nat] : Bool := Cases n of O => true | (S p) => (odd p) end
with odd [n:Nat] : Bool := Cases n of O => false | (S p) => (even p) end.

Print even.

Theorem even_Sn : (n:Nat)(even (S n))=(odd n).
Reflexivity.
Qed.

Theorem odd_Sn : (n:Nat)(odd (S n))=(even n).
Reflexivity.
Qed.

Theorem even_SSn : (n:Nat)(even (S (S n)))=(even n).
Intro;Rewrite even_Sn.
Rewrite odd_Sn.
Pattern (even n); Case (even n); Reflexivity.
Qed.

Section TreeForest.

Variable A : Set.

Mutual Inductive 
     tree   : Set := node : A -> forest -> tree
with forest : Set := empty : forest 
                  | cons : tree -> forest -> forest.

Check tree_rec.
Check forest_rec.

Fixpoint tree_size [t:tree] : Nat :=
         <Nat>Cases t of (node _ f) => (S (forest_size f)) end
with forest_size [f:forest] : Nat :=
         <Nat>Cases f of
                (cons t f1) => (plus (tree_size t) (forest_size f1))
              |    _   =>  O
         end.



Print tree_size.

Mutual Inductive Tree_Size : tree -> Nat -> Prop :=
  Node_Size : (n:Nat)(a:A)(f:forest)(Forest_Size f n)
               ->(Tree_Size (node a f) (S n))
with Forest_Size : forest -> Nat -> Prop :=
  Empty_Size : (Forest_Size empty O)
| Cons_Size : (n,m:Nat)(t:tree)(f:forest)
    (Tree_Size t n)->(Forest_Size f m)->(Forest_Size (cons t f) (plus n m)).

Hints Resolve Node_Size Empty_Size Cons_Size.

Theorem tree_size_prog : 
    (t:tree){n:Nat | (Tree_Size t n)}.
Proof.

Scheme tree_forest_rec := Induction for tree Sort Set
with   forest_tree_rec := Induction for forest Sort Set.

Check tree_forest_rec.
Check forest_tree_rec.

Intro.
Pattern t;
Apply tree_forest_rec with P0:=[f:forest]{n:Nat | (Forest_Size f n)}.
Induction 1; Intros n FSn.
Exists (S n); Auto.
Exists O; Auto.
Induction 1; Intros n TSn.
Induction 1; Intros m FSm.
Exists (plus n m); Auto.
Qed.

End TreeForest.
Print tree.

End NewInductifs.

(* $Id: NewInductifs.v,v 1.10 1999/06/29 07:48:38 loiseleu Exp $ *)
