1
(**********************************************************************)
2
(* A few examples showing the current limits of the conversion algorithm *)
3
(**********************************************************************)
5
(*** We define (pseudo-)divergence from Ackermann function ***)
7
Definition ack (n : nat) :=
8
(fix F (n0 : nat) : nat -> nat :=
13
(fix F0 (n2 : nat) : nat :=
16
| S n3 => F n1 (F0 n3)
20
Notation OMEGA := (ack 4 4).
22
Definition f (x:nat) := x.
24
(* Evaluation in tactics can somehow be controled *)
25
Lemma l1 : OMEGA = OMEGA.
26
reflexivity. (* succeed: identity *)
27
Qed. (* succeed: identity *)
29
Lemma l2 : OMEGA = f OMEGA.
30
reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *)
31
Abort. (* but it reduces the right side first! *)
33
Lemma l3 : f OMEGA = OMEGA.
34
reflexivity. (* succeed: reduce left side first *)
35
Qed. (* succeed: expected concl (the one with f) is on the left *)
37
Lemma l4 : OMEGA = OMEGA.
38
assert (f OMEGA = OMEGA) by reflexivity. (* succeed *)
39
unfold f in H. (* succeed: no type-checking *)
40
exact H. (* succeed: identity *)
41
Qed. (* fail: "f" is on the left *)
43
(* This example would fail whatever the preferred side is *)
44
Lemma l5 : OMEGA = f OMEGA.
46
assert (f OMEGA = OMEGA) by reflexivity.
49
Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *)
51
(**********************************************************************)
52
(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *)
53
(* (proof of span_ind_uninject_prop *)
55
In the proof, a problem of the form (Equal S t1 t2)
56
is "simpl"ified, then "red"uced to (Equal S' t1 t1)
57
where the new t1's are surrounded by invisible coercions.
58
A reflexivity steps conclude the proof.
60
The trick is that Equal projects the equality in the setoid S, and
61
that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)).
63
At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1)
64
and the algorithm is to first compare S and S', and t1 and t2.
65
Unfortunately it does not work, and since t1 and t2 involve concrete
66
instances of algebraic structures, it takes a lot of time to realize that
67
it is not convertible.
69
The only hope to improve this problem is to observe that S' hides
70
(behind two indirections) a Setoid constructor. This could be the
71
argument to solve the problem.