-
Notifications
You must be signed in to change notification settings - Fork 0
/
parcial2.v
227 lines (189 loc) · 5.76 KB
/
parcial2.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
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
(*
NOMBRE COMPLETO: Gabina Luz Bianchi
NRO. DE DOCUMENTO: 37447849
*)
Section Problema1.
Require Export List.
Require Export Arith.
Print beq_nat.
Set Implicit Arguments.
Fixpoint eliminar (z : nat) (l : list nat) : list nat :=
match l with
nil => nil
| cons x xs' => if (beq_nat x z) then xs' else cons x (eliminar z xs')
end.
Fixpoint pertenece (z : nat) (l : list nat) : bool :=
match l with
nil => false
| cons x xs' => if (beq_nat x z) then true else (pertenece z xs')
end.
Fixpoint concatenar (X: Set) (xs ys: list X) {struct xs}: list X := match xs with
nil => ys
| cons x xs' => cons x (concatenar xs' ys)
end.
Lemma L1_1 : forall (A : Set) (l : list A) (x : A), l <> x::l.
Proof.
intros.
induction l.
+ discriminate.
+ injection.
intros.
rewrite H1 in H0.
absurd(l = x :: l);assumption.
Qed.
Lemma L1_2 : forall (l1 l2 : list nat) (x : nat),
pertenece x (concatenar l1 l2) = true ->
pertenece x l1 = true \/ pertenece x l2 = true.
Proof.
induction l1; intros.
+ right.
auto.
+ simpl.
case_eq (beq_nat a x); intros.
- left.
reflexivity.
- apply IHl1.
inversion H.
rewrite -> H0.
reflexivity.
Qed.
Lemma L1_3 : forall (l : list nat) (x : nat),
pertenece x l = true -> eliminar x l <> l.
Proof.
induction l; intros.
+ discriminate.
+ simpl.
case_eq (beq_nat a x); intros.
- apply L1_1.
- injection.
intros.
inversion H.
rewrite H0 in H4.
absurd(eliminar x l = l).
* apply IHl.
assumption.
* assumption.
Qed.
End Problema1.
Section Problema2.
Inductive distintas (A:Set) : list A -> list A -> Prop :=
dist_base : distintas nil nil
| dist_induc : forall (a1 a2 : A) (l1 l2 :list A), a1 <> a2 -> distintas l1 l2 -> distintas (cons a1 l1) (cons a2 l2).
Hint Constructors distintas.
Require Import Coq.Bool.Bool.
(* Resolución 1*)
Lemma L2_2 : forall (l1 : list bool), { l2 : list bool | distintas l1 l2 }.
Proof.
intros.
induction l1.
+ exists nil.
auto.
+ elim IHl1; intros.
exists (cons (negb a) x).
constructor.
- unfold not.
intros.
apply (no_fixpoint_negb a) .
symmetry.
assumption.
- assumption.
Qed.
Lemma L2 : forall (l1 : list bool), { l2 : list bool | distintas l1 l2 }.
Proof.
intros.
induction l1.
+ exists nil.
auto.
+ elim IHl1; intros.
case_eq a; intros.
* exists (cons false x).
constructor.
- discriminate.
- assumption.
* exists (cons true x).
constructor.
- discriminate.
- assumption.
Qed.
End Problema2.
Extraction Language Haskell.
Extract Inductive bool => "Bool" [ "true" "false" ].
Extraction "distintas" L2.
Extraction "distintas2" L2_2.
Require Export List.
Require Export Arith.
Print beq_nat.
Set Implicit Arguments.
Section Problema3.
Definition Var := nat.
Definition Valor := nat.
Definition Memoria := Var -> Valor.
Definition lookup (m : Memoria) (v : Var) : Valor := m v.
Definition update (m : Memoria) (v : Var) (w : Valor) : Memoria := fun v0 : Var => if (beq_nat v0 v) then w else (m v0).
Inductive Instr : Set :=
assig : Var -> Valor -> Instr
| pC : Instr -> Instr -> Instr
| ifEq : Var -> Valor -> Instr -> Instr -> Instr.
Inductive Execute (m:Memoria): Instr -> Memoria -> Prop :=
xAss : forall (v:Var) (val:Valor), Execute m (assig v val) (update m v val)
| xSeq : forall (m1 m2 : Memoria) (i1 i2: Instr), Execute m i1 m1 -> Execute m1 i2 m2 -> Execute m (pC i1 i2) m2
| xIfT : forall (m':Memoria) (v1: Var) (i1 i2 :Instr) (val:Valor), lookup m v1 = val -> Execute m i1 m' -> Execute m (ifEq v1 val i1 i2) m'
| xIfF : forall (m':Memoria) (v1: Var) (i1 i2 :Instr) (val:Valor), lookup m v1 <> val -> Execute m i2 m' -> Execute m (ifEq v1 val i1 i2) m'.
Lemma L3_1 : forall (m1 m2 : Memoria) (var : Var) (val : Valor), Execute m1 (assig var val) m2 -> lookup m2 var = val.
Proof.
intros.
unfold lookup.
inversion H.
unfold update.
assert (beq_nat var var = true).
symmetry.
apply beq_nat_refl.
rewrite -> H3.
reflexivity.
Qed.
Lemma L3_2 : forall (m1 m2 : Memoria) (v : Var) (val : Valor) (i1 i2 : Instr), lookup m1 v <> val -> Execute m1 (ifEq v val i1 i2) m2 -> Execute m1 i2 m2.
Proof.
intros.
inversion H0.
+ absurd ( lookup m1 v = val); assumption.
+ assumption.
Qed.
Require Import Omega.
Theorem aux : forall (m : Memoria) (v1 v2 : Var) (val : Valor), v2 <> v1 -> update m v1 val v2 = m v2.
Proof.
intros.
unfold update.
case_eq (beq_nat v2 v1); intros.
- absurd (v2 = v1).
+ assumption.
+ apply (beq_nat_true v2 v1).
assumption.
- reflexivity.
Qed.
Lemma L3_3: forall (m1 m2 m3 : Memoria) (v1 v2 : Var) (val : Valor) (i1 i2 : Instr), v1 <> v2 -> Execute m1 (pC (assig v1 val) (assig v2 (val+1))) m2 -> Execute m2 i2 m3 -> Execute m2 (ifEq v2 (lookup m2 v1) i1 i2) m3.
Proof.
intros.
inversion H0.
apply xIfF.
+ inversion H6.
unfold lookup.
inversion H4.
unfold update.
case_eq (beq_nat v2 v2); intros.
- case_eq (beq_nat v1 v2); intros.
* absurd (v1 = v2).
assumption.
apply (beq_nat_true v1 v2).
assumption.
* assert (beq_nat v1 v1 = true).
symmetry.
apply (beq_nat_refl v1).
rewrite -> H15.
omega.
- assert (true = beq_nat v2 v2).
* apply (beq_nat_refl v2).
* rewrite H13 in H14.
discriminate.
+ assumption.
Qed.
End Problema3.