Un club privado tiene las siguientes reglas:
1. Todo miembro
no escocés lleva calcetines rojos
2. Todo miembro
lleva falda o no lleva calcetines rojos
3. los miembros
casados no salen los domingos
4. un miembro
sale los domingos si y solo si es escocés
5. todo miembro
que lleva falda es escocés y casado
6. todo miembro
escocés lleva falda
Coq < Section club.
Coq < Variable Escoces, CalcRojos, LLevaFalda, Casado,
SaleDomingo : Prop.
Escoces is assumed
CalcRojos is assumed
LLevaFalda is assumed
Casado is assumed
SaleDomingo is assumed
Coq < Hypothesis regla1 : ~Escoces -> CalcRojos.
regla1 is assumed
Coq < Hypothesis regla2 : LLevaFalda \/ ~CalcRojos.
regla2 is assumed
Coq < Hypothesis regla3 : Casado -> ~SaleDomingo.
regla3 is assumed
Coq < Hypothesis regla4 : SaleDomingo <->
Escoces.
regla4 is assumed
Coq < Hypothesis regla5 : LLevaFalda -> (Escoces
/\ Casado).
regla5 is assumed
Coq < Hypothesis regla6 : Escoces -> LLevaFalda.
regla6 is assumed
Coq < Lemma NoMember
: False.
1 subgoal
Escoces : Prop
CalcRojos : Prop
LLevaFalda : Prop
Casado : Prop
SaleDomingo : Prop
regla1 : ~Escoces->CalcRojos
regla2 : LLevaFalda\/~CalcRojos
regla3 : Casado->~SaleDomingo
regla4 : SaleDomingo<->Escoces
regla5 : LLevaFalda->Escoces/\Casado
regla6 : Escoces->LLevaFalda
============================
False
NoMember < Tauto.
Subtree proved!
Coq < End club.
2. Calculo de Predicados
Coq < Section Predicate_calculus.
Coq < Variable D:Set.
D is assumed
Coq < Variable R:D->D->Prop.
R is assumed
Supongamos que R es una relacion simetrica y transitiva.
Coq < Section R_sym_trans.
Coq < Hypothesis R_symmetric:(x,y:D) (R x y)
-> (R y x).
R_symmetric is assumed
Coq < Hypothesis R_transitive : (x,y,z:D)(R
x y) -> (R y z) -> (R x z).
R_transitive is assumed
Coq < Lemma refl_if
: (x:D)(EX y:D|(R x y))->(R x x).
1 subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x
z)
============================
(x:D)(EX y | (R x y))->(R x x)
refl_if < Print
ex.
Inductive ex [A : Set; P
: A->Prop] : Prop :=
ex_intro : (x:A)(P x)->(ex
A P)
----------------------------------------------
Coq < Inductive ex [A
: Set; P : A->Prop] : Prop :=
Coq < ex_intro : (x:A)(P x)->(ex
A P).
ex_ind is defined
ex is defined
Coq < Print ex_ind.
ex_ind =
[A:Set]
[P:A->Prop]
[P0:Prop]
[f:(x:A)(P x)->P0]
[e:(ex
A P)]<P0>Cases e of (ex_intro x x0) => (f x x0) end
: (A:Set)(P:A->Prop)(P0:Prop)((x:A)(P
x)->P0)->(ex A P)->P0
-----------------------------------------------
refl_if < Check
ex.
ex
: (A:Set)(A->Prop)->Prop
refl_if < Intros
x x_Rlinked.
1 subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x
z)
x : D
x_Rlinked : (EX y | (R x y))
============================
(R x x)
refl_if < Elim
x_Rlinked.
1 subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x
z)
x : D
x_Rlinked : (EX y | (R x y))
============================
(x0:D)(R x x0)->(R x x)
refl_if < Intros
y Rxy.
1 subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x
z)
x : D
x_Rlinked : (ex
D [y:D](R x y))
y : D
Rxy : (R x y)
============================
(R x x)
refl_if < Apply
R_transitive with y.
2 subgoals
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x
z)
x : D
x_Rlinked : (ex
D [y:D](R x y))
y : D
Rxy : (R x y)
============================
(R x y)
subgoal 2 is:
(R y x)
refl_if < Assumption.
1 subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x
z)
x : D
x_Rlinked : (ex
D [y:D](R x y))
y : D
Rxy : (R x y)
============================
(R y x)
refl_if < Apply
R_symmetric; Assumption.
Subtree proved!
refl_if is defined
Coq < End R_sym_trans.
Constant refl_if
: ((x,y:D)(R x y)->(R y x))
->((x,y,z:D)(R x y)->(R y z)->(R
x z))
->(x:D)(ex
D [y:D](R x y))->(R x x)