(* 
derivaciones
Reglas para el c'alculo de proposiciones y de predicados
Versi'on 0.3.a. Junio del 2005. Autor Luis Sierra 
Para Coq 8.0pl1 (Jul 2004) 

Modificaciones: .a m'as ejemplos.
*)

(* Una vez cargado este archivo, A y E quedan reservados como
símbolos de cuantificación. Ningún otro uso es aceptable. *)

(* Aceptamos lógica clásica *)

Require Classical_Prop.

(* Letras proposicionales *)

Parameters p p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 : Prop.
Parameters q q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 : Prop.
Parameters r r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 : Prop.
Parameters s s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 : Prop.

(* Universo *)

Parameter U : Set.

(* Símbolos de predicados *)

Parameter P Q R S P' Q' R' S' P'' Q'' R'' S'' : U -> Prop.
Parameters P2 Q2 R2 S2 P2' Q2' R2' S2' P2'' Q2'' R2'' S2'' : U * U -> Prop.
Parameters P3 Q3 R3 S3 P3' Q3' R3' S3' P3'' Q3'' R3'' S3'' : U * U * U -> Prop.

(* Símbolos de función *)

Parameters f g h f' g' h' f'' g'' h'' : U -> U.
Parameters f2 g2 h2 f2' g2' h2' f2'' g2'' h2'' : U * U -> U.
Parameters f3 g3 h3 f3' g3' h3' f3'' g3'' h3'' : U * U * U -> U.

(* Símbolos de constantes *)
(* Lateralmente, garantizan universo no vacío, 
porque para Coq son constantes *)

Parameters a b c d e : U.

(* Parameters x y z x1 y1 z1 : U. *)

(* Notación para cuantificadores *)

Notation "[ 'A' x ] B" := (forall x:U, B) (at level 72, right associativity).
Notation "[ 'E' x ] B" := (exists x:U, B) (at level 72, right associativity).

Module Err.

Ltac ERR1 := (fail 1 
  "El lado izquierdo de la conjunción no coincide con la conclusión.").
Ltac ERR2 := (fail 1 
  "El lado derecho de la conjunción no coincide con la conclusión.").
Ltac ERR3 := (fail 1
  "La fórmula ingresada no se corresponde con la conclusión.").

Ltac ERRHip :=    (fail 0 "Hipótesis inexistente.").
Ltac ERRInY :=    (fail 0 "La conclusión de YI debe ser una conjunción.").
Ltac ERRInO :=    (fail 0 "La conclusión de OI debe ser una disyunción.").
Ltac ERRInSi :=   (fail 0 "La conclusión de SiI debe ser una implicación.").
Ltac ERRInSii :=  (fail 0 "La conclusión de SiiI debe ser una implicación.").
Ltac ERRInNo :=   (fail 0 "La conclusión de NoI debe ser una implicación.").
Ltac ERRElimY :=  (fail 0 "Debe eliminar una conjunción.").
Ltac ERRElimO :=  (fail 0 "Debe eliminar una disyunción.").
Ltac ERRElimNo := (fail 0 "La conclusión debe ser False.").
Ltac ERRElimPT := (fail 0 "Debe eliminar una cuantificación universal.").

End Err.

Module Aux.

(* Lemas necesarios para las reglas de 
inferencia del Sii *)

Lemma LSiiE1 : forall A B : Prop, (A <-> B) -> A -> B.
induction 1 as (k,l); exact k. Qed.

Lemma LSiiE2 : forall A B : Prop, (A <-> B) -> B -> A.
induction 1 as (k,l); exact l. Qed.

(* Nucleo de las reglas de inferencia *)

Ltac Hip := assumption.
Ltac RAA := apply Classical_Prop.NNPP; intro.

Ltac YI := constructor.
Ltac YE1 f := 
  let pko := fresh
    in (assert (pko : f); [idtac | (exact (proj1 pko) || Err.ERR1)]).
Ltac YE2 f := 
  let pko := fresh
    in (assert (pko : f); [idtac | (exact (proj2 pko) || Err.ERR2)]).
Ltac OI1 := constructor 1.
Ltac OI2 := constructor 2.
Ltac OE f := let pko := fresh in (assert (pko : f); [idtac | (induction pko)]).
Ltac SiI := intro.
Ltac SiE f := cut f.
Ltac SiiI := constructor; intro.
Ltac SiiE1 f := apply LSiiE1 with f.
Ltac SiiE2 f := apply LSiiE2 with f.
Ltac NoI := intro.
Ltac NoE f := cut f; fold (~f).
Ltac BotE := absurd False; [tauto | idtac].
Ltac PTE f x := 
  let pko := fresh 
    in (assert (pko : f); [ idtac | (exact (pko x) || Err.ERR3)]).
Ltac PTI := intro.

Ltac EXI x := exists x.
Ltac EXE f := 
  let pko := fresh
    in (assert (pko : f); [idtac | elim pko; intros; clear pko]).


End Aux.

(* Reglas de inferencia *)
(* El nombre de la regla se construye con: 
nombre de conector + tipo de regla + eventualmente variante.
Nombres de conectores: Y O Si Sii No Bot PT EX
Tipo de regla: I E
Variante: 1 2.
Otras reglas: Hip RAA *)

Ltac Hip := Aux.Hip || Err.ERRHip.
Ltac RAA := Aux.RAA.
Ltac YI := match goal with | |- _ /\ _ => Aux.YI end ||  Err.ERRInY.
Ltac YE1 f := match f with | _ /\ _ => Aux.YE1 f end || Err.ERRElimY.
Ltac YE2 f := match f with | _ /\ _ => Aux.YE2 f end || Err.ERRElimY.
Ltac OI1 := match goal with | |- _ \/ _ => Aux.OI1 end || Err.ERRInO.
Ltac OI2 := match goal with | |- _ \/ _ => Aux.OI2 end || Err.ERRInO.
Ltac OE f := match f with | _ \/ _ => Aux.OE f end || Err.ERRElimO.
Ltac SiI := match goal with | |- _ -> _ => Aux.SiI end || Err.ERRInSi.
Ltac SiE f := Aux.SiE f.
Ltac SiiI := match goal with | |- _ <-> _ => Aux.SiiI end || Err.ERRInSii.
Ltac SiiE1 f := Aux.SiiE1 f.
Ltac SiiE2 f := Aux.SiiE2 f.
Ltac NoI := match goal with | |- ~_ => Aux.NoI end || Err.ERRInNo.
Ltac NoE f := match goal with | |- False => Aux.NoE f end || Err.ERRElimNo.
Ltac BotE := Aux.BotE.
Ltac PTE x f := match f with | ([ A x] _) => Aux.PTE f x end || Err.ERRElimPT.
Ltac PTI := Aux.PTI || (fail 0 ).
Ltac EXI x := Aux.EXI x || (fail 0 ).
Ltac EXE f := Aux.EXE f || (fail 0 ).


Theorem T1732: (p \/ q) <-> ~(~p /\ ~q).
SiiI.
NoI.
OE (p \/ q).
Hip.
NoE p.
YE1 (~p /\ ~q). Hip. Hip.
NoE q.
YE2 (~p /\ ~q).  Hip. Hip.

RAA. NoE (~p /\ ~q). Hip. YI. NoI. NoE (p \/ q). Hip.
OI1. Hip. NoI. NoE (p \/ q). Hip.
OI2. Hip.

Show Script. Show Proof.

Qed.

Theorem T1734: (p /\ q) <-> ~(~p \/ ~q).
SiiI. NoI. OE (~p \/ ~q). Hip. NoE p. Hip. YE1 (p /\ q).
Hip.
NoE q. Hip. YE2 (p /\ q). Hip.
YI. RAA. NoE (~p \/ ~q). Hip. OI1. Hip. 
RAA. NoE (~p \/ ~q). Hip. OI2. Hip.
Qed.

(* Ejemplos *)

Lemma vg1: (p /\ q -> r) -> p -> q -> r.
SiI.
SiI.
SiI.
SiE (p /\ q).
 Hip.
 YI.
  Hip.
  Hip.
Qed.

Print vg1.

Lemma vg1': (p /\ q -> r) -> p -> q -> r.
repeat SiI; SiE (p /\ q); [Hip | YI; Hip].
Qed.

Lemma vg2: p \/ q -> q \/ p.
SiI.
OE (p \/ q).
 Hip.
 OI2.
   Hip.
 OI1.
   Hip.
Qed.

Lemma vg3: ((p -> q) -> p) -> p.
SiI.
RAA.
NoE p.
 Hip.
 SiE (p -> q).
  Hip.
  SiI.
    BotE.
    NoE p.
   Hip.
   Hip.
Qed.

Lemma vg3': ((p -> q) -> p) -> p.
SiI; RAA; NoE p; [ Hip | SiE (p -> q); [ Hip | SiI; BotE; NoE p; Hip ]].
Qed.

Lemma vg4: [E x][A y] P2(x,y) -> [A y][E x] P2(x,y).
SiI.
EXE ([ E x][ A y]P2 (x, y)).
 Hip.
 EXI x.
   PTE y ([ A y]P2 (x, y)).
   Hip.
Qed.

Lemma vg4': [E x][A y] P2(x,y) -> [A y][E x] P2(x,y).
SiI.
PTI.
EXE ([ E x][ A y]P2 (x, y)).
 Hip.
 EXI x.
   PTE y ([ A y]P2 (x, y)).
   Hip.
Qed.

Lemma vg5: [A x][A y] P2(x,y) -> [A x] P2(x,x).
SiI.
PTI.
PTE x ([ A y]P2 (x, y)).
PTE x ([ A x][ A y]P2 (x, y)).
Hip.
Qed.

Lemma vg5': [A x][A y] P2(x,y) -> [A x] P2(x,x).
SiI.
PTI.
PTE y ([ A y]P2 (x, y)).
PTE x ([ A x][ A y]P2 (x, y)).
Hip.
Qed.

Lemma vg6: [A x](P x -> Q x) -> [A x] P x -> [A x] Q x.
SiI.
SiI.
PTI.
SiE (P x).
 PTE x ([ A x](P x -> Q x)).
   Hip.
 PTE x ([ A x]P x).
   Hip.
Qed.

Lemma vg7: [A x] P(x) -> [E x]P(x).
SiI.
EXI a.
PTE a ([ A x]P x).
Hip.
Qed.