-
Notifications
You must be signed in to change notification settings - Fork 0
/
tp3.v
152 lines (116 loc) · 3.53 KB
/
tp3.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
(* Trabajo Práctico 3 *)
(* Gabina Luz Bianchi *)
Section Ejercicio3. (* Necesito la definición de o para el ejrcicio 4 *)
Variable A B C: Set.
Definition apply := fun (A B : Set) (f: A->B) => fun a:A => (f a).
Definition o := fun (A B C : Set) (f: A->B) => fun g: B->C => fun a:A => ( g (f a)).
Definition twice := fun (A : Set) (f: A->A) => fun a:A => (f (f a)).
End Ejercicio3.
Section Ejercicio4.
Variable A: Set.
Definition id := fun (A : Set) (x : A) => x.
(* Prueba 1 *)
Theorem e41 : forall x:A, (o A A A (id A) (id A) x) = (id A x).
Proof.
intros.
compute.
reflexivity.
Save.
(* Prueba 2 *)
Theorem e42 : forall x:A, (o A A A (id A) (id A) x) = (id A x).
Proof.
intros.
cbv delta beta.
reflexivity.
Save.
(* Prueba 3 *)
Theorem e43 : forall x:A, (o A A A (id A) (id A) x) = (id A x).
Proof.
intros.
cbv delta.
simpl.
reflexivity.
Save.
End Ejercicio4.
Section Ejercicio5.
(* 5.1 *)
Definition opI (A : Set) (x : A) := x.
Definition opK (A B: Set) (x : A) (y : B) := x.
Definition opS (A B C : Set) (f : A -> B -> C) (g: A -> B) (x : A) := ((f x) (g x)).
Check opI.
Check opK.
Check opS.
(* 5.2 *)
(* Para formalizar el siguiente lema, determine los tipos ?1 ... ?8 adecuados *)
Lemma e52 : forall (A B : Set), opS A (B -> A) A (opK A (B -> A)) (opK A B) = (opI A).
Proof.
intros.
compute.
reflexivity.
Save.
End Ejercicio5.
Section Ejercicio10.
Parameter Array : Set -> nat -> Set.
Parameter emptyA : forall X : Set, Array X 0.
Parameter addA : forall (X : Set) (n : nat), X -> Array X n -> Array X (S n).
Parameter Matrix : Set -> nat -> Set.
Parameter emptyM : forall X:Set, Matrix X 0.
Parameter addM : forall (X:Set) (n:nat), Matrix X n -> Array X (n + 1) -> Matrix X (n+1).
Definition A1 := (addA nat 0 1 (emptyA nat)).
Check A1.
Definition M1 := addM nat 0 (emptyM nat) A1. (* matriz de una columna *)
Check M1.
Definition A2 := (addA nat 1 2 ((addA nat 0 2 (emptyA nat)))).
Check A2.
Definition M2 := addM nat 1 M1 A2. (* matriz de dos columnas *)
Check M2.
Definition A3 := addA nat 2 3 (addA nat 1 3 ((addA nat 0 3 (emptyA nat)))).
Check A3.
Definition M3 := addM nat 2 M2 A3. (* matriz de tres columnas *)
Check M3.
End Ejercicio10.
Section Ejercicio11.
Parameter ABNat : forall n : nat, Set.
Parameter emptyAB : ABNat 0.
Parameter addAB : forall n : nat, ABNat n -> ABNat n -> nat -> ABNat (n+1).
Definition BT1 := addAB 0 emptyAB emptyAB 7. (*Árbol binario de altura 1 cuya raíz es 7*)
Check BT1.
Definition BT2 := addAB 1 BT1 BT1 3.
Check BT2.
Parameter ABtype : forall (X: Set) (n : nat), Set.
Parameter emptyABtype : forall X: Set, ABtype X 0.
Parameter addABtype : forall (X: Set) (n : nat), ABtype X n -> ABtype X n -> X -> ABtype X (n+1).
Check addABtype.
End Ejercicio11.
Section Ejercicio15.
Variable U : Set.
Variable e : U.
Variable A B : U -> Prop.
Variable P : Prop.
Variable R : U -> U -> Prop.
Lemma Ej315_1 : (forall x : U, A x -> B x) -> (forall x : U, A x) ->
forall x : U, B x.
Proof.
intros.
exact (H x (H0 x)).
Save.
Lemma Ej315_2 : forall x : U, A x -> ~ (forall x : U, ~ A x).
Proof.
unfold not.
intros.
exact (H0 x H).
Save.
Lemma Ej315_3 : (forall x : U, P -> A x) -> P -> forall x : U, A x.
Proof.
exact (fun (H : forall x : U, P -> A x) (H0 : P) (x : U) => (H x H0)).
Save.
Lemma Ej315_4 : (forall x y : U, R x y) -> forall x : U, R x x.
Proof.
exact (fun (H :forall x y : U, R x y) (x : U) => (H x x)).
Save.
Lemma Ej315_5 : (forall x y: U, R x y -> R y x) ->
forall z : U, R e z -> R z e.
Proof.
exact (fun (H : forall x y:U, R x y -> R y x) (z : U) => (H e z)).
Save.
End Ejercicio15.