Section Pairs.

Variables A, B : Set.

Inductive Pair : Set := mkPair : A -> B -> Pair.

Check Pair.


Fixpoint proj1 [p:Pair] : A :=
       Cases p of
          (mkPair x _) => x
       end.


Fixpoint proj2 [p:Pair] : B :=
       Cases p of
          (mkPair _ y) => y
       end.

Check proj1.

End Pairs.

Print Pair.
Check Pair.
Check mkPair.
Print proj1.

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

Reset Pairs.

Inductive Pair [A:Set; B:Set] : Set :=
                      mkPair : A -> B -> (Pair A B).



Fixpoint proj1 [A:Set; B:Set; p: (Pair A B)] : A := 
       Cases p of
          (mkPair x _) => x
       end.
 
Fixpoint proj2 [A:Set; B:Set; p: (Pair A B)] : B := 
       Cases p of
          (mkPair _ y ) => y
       end.
 

(* NOTAR que na concordancia de padroes de elementos de um tipo indutivo parametrizado, os construtores nao esperam os parametros do tipo como argumento. O valor desses parametros eŽ calculado automaticamente pelo sistema.
Assim, escrevemos (mkPair x _) em vez de (mkPair A B x _) *) 

Print Pair.
Print proj1.

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

Inductive PAir : Set -> Set -> Set :=
        mkPAir : (A,B:Set) A -> B -> (PAir A B).

Reset PAir.

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


Theorem eq1 : (A,B:Set)(p:(Pair A B))
                (mkPair A B (proj1 A B p) (proj2 A B p)) = p.

Intros.
Check Pair_ind.
Elim p.
Intros.
Simpl.
Reflexivity.

(*
Undo 3.
Auto.
*)

Save.

Check Pair_ind.

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

Theorem eq2 : (A,B:Set)(x:A)(y:B) (proj1 A B (mkPair A B x y)) = x.
 
Proof.
Intros.
Simpl.
Reflexivity.

Restart.
Auto.

Qed.

(* ------- Questao 10A -------- *)

Fixpoint f [A:Set; p:(Pair A A)] : (Pair A (Pair A A)) :=
      Cases p of
         (mkPair x y) => (mkPair A (Pair A A) x (mkPair A A x y))
      end.

Print f.

Theorem q10A : (A:Set)(p:(Pair A A)) 
                  (f A p) = (mkPair A (Pair A A) (proj1 A A p) p).

Proof.
Intros.
Elim p.
(* Case p.    era equivalente ... *)
Simpl.
Intros.
Reflexivity.

Qed.

(* ------- Questao 10B -------- *)

Fixpoint ff [A:Set; p:(Pair A A)] : (Pair (Pair A A) A) :=
      Cases p of
         (mkPair x y) => (mkPair (Pair A A) A (mkPair A A x y) y)
      end.

Print ff.

Theorem q10B : (A:Set)(p:(Pair A A)) 
                  (ff A p) = (mkPair (Pair A A) A p (proj2 A A p)).

Proof.
Intros.
Elim p.
(* Case p.    era equivalente ... *)
Simpl.
Intros.
Reflexivity.

Qed.

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

Inductive List [A:Set] : Set :=
      nil  : (List A)
    | cons : A -> (List A) -> (List A).

Check List.
Check cons.
Check nil.


Fixpoint cat [A:Set; l:(List A)] : (List A) -> (List A) :=
      [l':(List A)] Cases l of
                        nil      => l'
                    | (cons h t) => (cons A h (cat A t l'))
                    end.   


Fixpoint rev [A:Set; l:(List A)] : (List A) :=
           Cases l of
               nil      => (nil A)
           | (cons h t) => (cat A (rev A t) (cons A h (nil A)))
           end.   


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

Lemma lemma1 : (A:Set)(l:(List A))(cat A l (nil A)) = l.

Intro.
Induction l; Clear l.
Auto.
Intros.
Simpl.
Rewrite H.
Auto.

Save.

Hint lemma1.

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

Reset List.

Section SetA.

Variable A : Set.

Inductive List : Set :=
           nil : List
        | cons : A -> List -> List.

Fixpoint cat [l:List] : List -> List :=
     [l':List] Cases l of 
                 nil  => l'
               | (cons h t) => (cons h (cat t l'))
               end.

Fixpoint rev [l:List] : List :=
            Cases l of 
               nil   => nil
            | (cons h t) => (cat (rev t) (cons h nil))
            end.

Token "::".
Token "@".
Infix 7 "::" cons.
Infix 6 "@" cat.

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

Lemma lemma1 : (l:List)((l @ nil) = l).

Induction l; Clear l.
Auto.
Intros.
Simpl.
Rewrite H.
Auto.

Save.
Hint lemma1.

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

Theorem catAssoc : (l1,l2,l3:List)
              (l1 @ (l2 @ l3)) = (cat (l1 @ l2) l3).

Induction l1; Clear l1.
Auto.
Intros.
Simpl.
Rewrite H.
Auto.

Save.
Hint catAssoc.

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

Theorem revCat : (l1,l2:List)
          (rev (l1 @ l2)) = (cat (rev l2) (rev l1)).

Induction l1; Clear l1.
Intro.
Simpl.
Rewrite lemma1; Auto.
Intros.
Simpl.
Rewrite H.
Auto.

Save.

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

Print nat.
Print plus.
Print mult.
Print pred.
Print le.


Fixpoint comp [l:List] : nat := 
         <nat>Cases l of 
                 (cons _ m) => (S (comp m)) 
                |  _        => O 
         end.


(* --- Questao 11A --- *)

Theorem q11A : (x:A)(l:List)(le (comp l) (comp (cons x l))).

Proof.
Induction l.
Simpl.
Auto.
(*   Equivalentemente ...
   Print le.
Apply le_S.
Apply le_n.
*)

Intros.
Simpl.
Auto.

Qed.


(* --- Questao 11B --- *)

Theorem q11B : (l,l':List)(comp (l @ l'))= (plus (comp l) (comp l')).

Proof.
Induction l.
Simpl.
Reflexivity.

Intros.
Simpl.
Rewrite H.
Auto.

Qed.

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

Theorem revrev : (l:List)(rev (rev l)) = l.

Proof.

Induction l.
Simpl.
Auto.

Intros.
Simpl.
Rewrite revCat.
Rewrite H.
Simpl.
Auto.

Qed.

(* Experimentar 
Focus. 
 e 
Unfocus. 
*)

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

Fixpoint member [l:List] : A -> Prop :=
     [x:A] Cases l of
              nil       => False
           | (cons h t) => (x=h) \/ (member t x)
           end.

Fixpoint member2 [x:A; l:List] : Prop :=
           Cases l of
              nil   => False
           | (cons h t) => (x=h) \/ (member2 x t)
           end.

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

Theorem membcat1 : (l1,l2:List) (x:A)
          (member l1 x) \/ (member l2 x) -> (member (l1 @ l2) x).

Induction l1; Clear l1.
Intros.
Simpl.
Elim H; Clear H.
Intro H.
Elim H.
Auto.
Intros a l H l2 x.
Simpl.
Intro H0.
Elim H0; Clear H0.
Intro H0; Elim H0; Clear H0.
Auto.

Intro H0.
Right.
Apply H.
Auto.

Intro H0.
Right.
Apply H.
Auto.

Save.

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


Inductive memberP : List -> A -> Prop :=
   memberPhead : (x,h:A)(t:List) 
                 (x=h) -> (memberP (cons h t) x)
 | memberPtail : (x,h:A)(t:List) 
                 (memberP t x) -> (memberP (cons h t) x).

Hint memberPhead memberPtail.

(*
Inductive memberP : List -> A -> Prop :=
    memberPnil : (x:A) ~(memberP nil x)
 | memberPhead : (x,h:A)(t:List) 
                 (x=h) -> (memberP (cons h t) x)
 | memberPtail : (x,h:A)(t:List) 
                 (memberP t x) -> (memberP (cons h t) x).
*)

Theorem membPcat1 : (l1,l2:List) (x:A) 
              (memberP l1 x)\/(memberP l2 x)->(memberP l1 @ l2 x).

Intros l1 l2 x H.
Elim H; Clear H.
Intro H.

Check memberP_ind.

Elim H; Clear H.
Simpl.
Intros.
Rewrite H.
Apply memberPhead.

Undo 4.

Simpl; Auto.
Simpl; Auto.

Elim l1; Clear l1.
Auto.
Simpl; Auto.

Save.

(* ---------- Exercicio ----------- *)
(*
Inductive revP : List -> List -> Prop :=
      revPnil : (revP nil nil)
   | revPcons : (h:A)(t,tr,lh:List) 
       (revP t tr) -> (lh = (cat tr (cons h nil))) ->
                (revP (cons h t) lh).

Hint revPnil revPcons.


Theorem revRevP : (l,lr:List) (revP l lr) -> (revP lr l).

............

*)


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


End SetA.

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

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


Print eq.
Check eq.
Check eq_ind.