blob: 88848121027a41996cbd6fcb341c2c38f9fb3e49 (
plain)
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
|
Require Coq.Program.Tactics.
Record Matrix (m n : nat).
Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q):
Matrix (m*p) (n*q). Admitted.
Fail Program Fact kp_assoc
(xr xc yr yc zr zc: nat)
(x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
kp x (kp y z) = kp (kp x y) z.
Ltac Obligation Tactic := admit.
Fail Program Fact kp_assoc
(xr xc yr yc zr zc: nat)
(x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
kp x (kp y z) = kp (kp x y) z.
Axiom cheat : forall {A}, A.
Obligation Tactic := apply cheat.
Program Fact kp_assoc
(xr xc yr yc zr zc: nat)
(x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
kp x (kp y z) = kp (kp x y) z.
admit.
Admitted.
|
