(* Marco 1998                                 *)
(* ****************************************** *)
(* 	              COQ      		      *)
(* 					      *)
(* 

O Coq e' um sistema de prova assistida para logicas de ordem superior, 
que permite o desenvolvimento de programas de modo consistente com a 
sua especificacao (programas certificados).

Partes a realcar no Coq:  a linguagem logica, o sistema de prova e 
o extractor de programas.

O Coq baseia-se no Calculo de Constrocoes Indutivas. Vai-se, portanto, 
trabalhar no lambda-calculus com tipos.

Existem 3 especies de especificacoes:
  Prop - proposicoes logicas
  Set  - coleccoes matematicas
  Type - tipos abstractos

Por especificacao entende-se a expressao que classifica o objecto que 
esta' a ser declarado.

Um contexto e' uma sequencia de declaracoes/definicoes.
O que se declara/define, a cada instante, no contexto so' pode depender 
daquilo que esta' declarado para tra's.
*)

(* ****************************************** *)
(* athena                                     *)
(* 					      *)
(* export PATH=${PATH}:/usr1/ML/ocaml/COQ/bin *)
(* 					      *)
(* coqtop				      *)
(* Load __.         carrega o ficheiro __.v   *)



(* Declaracoes *)

Variable nat : Set.
Variable x, y, a, b, um : nat.

Variables m, n : nat.

Variable soma : nat -> nat -> nat.


(* Aplicacoes *)

Check soma.
Check (soma n).
Check ((soma n) m).    
Check (soma n m).    
Check (soma x x).


(* Abstraccoes *)

Check [x:nat](soma x x).
Check [y:nat](soma y).
Check [y:nat](soma y x).

(* Definicoes *)

Definition id := [x:nat]x.
Definition inc := [x:nat](soma um x).
Definition mais := [y:nat][x:nat](soma x y).

Print id.
Print inc.
Print mais.

(* Reducoes *)

Eval (([x:nat](soma um x)) y).
(*V6.2****      Eval Cbv Beta in (([x:nat](soma um x)) y). *)

Eval (inc y).
(*V6.2****      Eval Cbv Beta in (inc y). *)

Compute (inc y).
(*V6.2****      Eval Compute in (inc y). *)
(*V6.2****      Eval Cbv Beta Delta [inc] in (inc y). *)

Compute (mais um um).

Eval (([x:nat](soma um x)) (soma um y)).

Eval (([x:nat][a:nat](soma a x)) y b).


(* --------------- estudar o caso ------------
Definition M := (soma um x).
Definition N := [x:nat] M.
Compute (N a).
------------------------------------------- *)



(* **** Comandos ********************************* 

Print __.         mostra a definicao/declaracao de __
Print All.        mostra a definicao/declaracao de tudo o que esta' no contexto

Reset __.         apaga todo o contexto ate __ 
Reset Initial.    apaga tudo do contexto

Check __.         da' o tipo 
Eval __.          da' a forma beta-normal de __
Compute __.       da' a forma beta/delta-normal de __

Quit.             para sair do coq  

*********************************************** *)



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

Variables A, B, C : Prop.

Goal A->B->A.
Intros.
Assumption.
Save teo1.


Theorem  teo2 : (A->B)->(B->C)->A->C.
Intros.
Apply H0.
Apply H.
Exact H1.
Qed.


Lemma  teo3 : (A->B)->A->B.
Auto.
Qed.


(* **** Comandos ********************************* 

Undo.     desfaz o ultimo passo da prova
Show.     mostra o estado da prova
Abort.    sai da prova

*********************************************** *)