Section Natural.

Variable natural : Set.
Variable zero : natural.
Variable suc : natural -> natural.
Variables soma, prod : natural -> natural -> natural.

Infix 8 "+" soma.
Infix 9 "*" prod.



Hypothesis s_ne_z : (x:natural) ~(suc x) = zero.
Hypothesis suc_inj : (x,y:natural)
                     (suc x) = (suc y) -> x = y.

Hypothesis Sum1 : (x:natural) (soma zero x) = x. 
Hypothesis Sum2 : (x,y:natural)
                  (soma (suc y) x) = (suc (soma y x)). 
Hypothesis Prod1 : (x:natural) (prod zero x) = zero.
Hypothesis Prod2 : (x,y:natural)
                   (prod (suc y) x) = (soma x (prod y x)).

Hypothesis induct : (P:natural->Prop)
                    (P zero) -> ((x:natural)(P x) -> (P (suc x))) 
                    -> (x:natural)(P x).


(* ---------- *)

Theorem trans : (A:Set)(x,y,z:A) x=y -> y=z -> x=z.

Intros A x y z H H0.
Rewrite H.
Undo.
Rewrite <- H0.
Auto.

Abort.


(* ---------- *)

Theorem dois : (suc (suc zero)) = (soma (suc zero)(suc zero)).

Rewrite Sum2; Rewrite Sum1; Reflexivity.

Restart.

Lemma SucCong : (x,y:natural) x=y -> (suc x) = (suc y).

Intros x y H; Rewrite H; Reflexivity.
Save.

Hint SucCong.
Print Hint.

Rewrite Sum2; Auto.
Save.

(* ---------- *)

Theorem um : (prod (suc zero) (suc zero)) = (suc zero).

Rewrite Prod2; Rewrite Sum2; Rewrite Prod1; Auto.

Save.

(* ---------- *)

Theorem Sum1r : (n:natural) (soma n zero) = n.

Intro n; Apply induct with x:=n; [Auto | Intros x H; Rewrite Sum2; Auto].

Save.

Hint Sum1r.                
 
(* ---------- *)

Theorem Sum2r : (m,n:natural)
                (soma m (suc n)) = (suc (soma m n)).

Intros m n; Apply induct with x:=m;
[Rewrite Sum1; Auto | Intros x H; Rewrite Sum2; Rewrite Sum2; Auto].
 
Save.

Hint Sum2r.

(* ---------- *)

Theorem inicial : (n:natural)
                  (n=zero) \/ (Ex [x:natural] n=(suc x)).
Intro n.
Apply induct with x:=n;
 [ Left; Auto 
 | Intros x H; Elim H; 
    [ Clear H; Intro H; Right; Exists zero; Auto 
    | Clear H; Intro H; Right; Elim H; Clear H; 
      Intros x0 H; Exists (suc x0); Auto
    ]
 ].

Save.

(* ---------- *)

(* ------------- Questao ------------ *)

Theorem comSum : (x,y:natural) (soma x y) = (soma y x).

Intro x.
Apply induct with x:=x.
 Intro.
 Rewrite Sum1.
 Auto.                   (* fim do ramo 1 *)
Intros.
Rewrite Sum2.
Rewrite Sum2r.
Auto.

Qed.

(* ------------- Questao ------------ *)

Theorem Prod1r : (x:natural) (prod x zero) = zero.

Intro.
Apply induct with x:=x.
Apply Prod1.
Intros.
Rewrite Prod2.
Rewrite Sum1.
Assumption.

Qed.


Reset Natural.            


(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)

Section Nati.

Inductive nati : Set := zero : nati 
                      | suc  : nati -> nati.

(* ---------- *)

Theorem SucCong : (x,y:nati) x=y -> (suc x) = (suc y).

Intros x y H; Rewrite H; Auto.

Save.

Hint SucCong.

Check nati_ind.

(* ---------- *)

Theorem inicial : (n:nati) 
                  (n=zero) \/ (Ex [x:nati] n=(suc x)).
Intro n. 
Apply nati_ind with n:=n.

Undo.
Elim n. 

Restart.
Induction n.
Left; Auto.
Intros.
Right; Elim H;
[ Intros; Exists zero; Auto 
| Intro; Exists n0; Auto ].

Save.

(* ---------- *)

Theorem suc_inj : (x,y:nati) (suc x) = (suc y) -> x = y.

Intros x y H; Injection H; Auto.

Save.

(* ---------- *)

Theorem s_ne_z : (x:nati) ~(suc x) = zero.

Intro; Discriminate.

Save.

(* ---------- *)

Check nati_rec.

(* ---------- *)

Fixpoint soma [n:nati] : nati -> nati :=
   [m:nati] Cases n of
                zero   => m
            |  (suc p) => (suc (soma p m))
            end.   


Fixpoint prod [n:nati] : nati -> nati :=
   [m:nati] Cases n of
               zero   => zero
            | (suc p) => (soma m (prod p m))
            end.  

(* ---------- *)
Check soma.
Check prod.
Check   [n,m:nati] Cases n of
                zero   => m
            |  (suc p) => (suc (soma p m))
            end.  
(* ---------- *)

Theorem dois : (suc (suc zero)) = (soma (suc zero) (suc zero)).

Simpl.
Reflexivity.

Save.

(* ---------- *)

Theorem um : (prod (suc zero) (suc zero)) = (suc zero).
Simpl; Reflexivity.

Save.

(* ---------- *)

Theorem Sum1r : (n:nati) (soma n zero) = n.

Induction n; [Simpl; Auto | Simpl; Auto ].

Restart.
Induction n; Simpl; Auto.

Save.

Hint Sum1r.

(* ---------- *)

Theorem Sum2r : (m,n:nati) (soma m (suc n)) = (suc (soma m n)).

Induction m; Simpl; Auto. 

Save.

Hint Sum2r.

(* ---- Questao ------ *)

Theorem comSum : (n,m:nati) (soma n m) = (soma m n).

Proof.
Induction n.
  Simpl.
  Auto.

  Simpl.
  Intros.
  Rewrite Sum2r. 
  Auto.

Qed.

(* ---- Questao ------ *)

Theorem Prod1r : (x:nati) (prod x zero) = zero.

Proof.
Induction x.
Auto.

Simpl.
Auto.


Restart.
Induction x; Simpl; Auto.

Qed.

(* ---------- *)

Fixpoint pred [d:nati] : nati -> nati :=
   [n:nati] Cases n of
              zero    => d
            | (suc p) => p
            end.


(* ------ Exercicio  ------- *)

Theorem ex1 : (x:nati) (suc (pred zero x)) = x.

Induction x.
Simpl.
Abort.

(* ---------- *)

Theorem ex2 : (x:nati) (pred zero (suc x)) = x.

Proof.
Induction x.
Simpl.
Trivial.

Intros.
Simpl.
Trivial.

Restart.
Auto.

Qed.

(* ------ Exercicio  ------- *)

Fixpoint factorial [n:nati] : nati :=
      Cases n of
         zero   => (suc zero)
      | (suc p) => (prod (suc p) (factorial p))
      end.


Eval Compute in (factorial (suc (suc (suc zero)))).         



Fixpoint fact_errado1 [n:nati] : nati :=
      Cases n of
          (suc p) => (prod (suc p) (fact_errado1 p))
      end.


Fixpoint fact_errado2 [n:nati] : nati :=
      Cases n of
         zero   => (suc zero)
      | (suc p) => (prod (suc p) (fact_errado2 (suc p)))
      end.



(* ---------------------- *)

Fixpoint max [n,m:nati] : nati :=
        Cases n of 
            zero   => m
        |  (suc p) => Cases m of 
                           zero   => (suc p)
                      |   (suc q) => (suc (max p q))
                      end
        end.        

Fixpoint max_alt [n,m:nati] : nati :=
      Cases n m of 
             zero    _      => m
        |   (suc p)  zero   => (suc p)
        |   (suc p) (suc q) => (suc (max_alt p q))
       end.    
    
Fixpoint max_alt3 [n:nati] : nati ->nati :=
   [m:nati]  Cases n m of 
             zero    _          => m
        |   ((suc p) as N) zero => N
        |   (suc p) (suc q)     => (suc (max_alt3 p q))
       end.