summaryrefslogtreecommitdiff
path: root/dev/doc/notes-on-conversion.v
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
commit9043add656177eeac1491a73d2f3ab92bec0013c (patch)
tree2b0092c84bfbf718eca10c81f60b2640dc8cab05 /dev/doc/notes-on-conversion.v
parenta4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff)
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'dev/doc/notes-on-conversion.v')
-rw-r--r--dev/doc/notes-on-conversion.v73
1 files changed, 73 insertions, 0 deletions
diff --git a/dev/doc/notes-on-conversion.v b/dev/doc/notes-on-conversion.v
new file mode 100644
index 00000000..a81f170c
--- /dev/null
+++ b/dev/doc/notes-on-conversion.v
@@ -0,0 +1,73 @@
+(**********************************************************************)
+(* A few examples showing the current limits of the conversion algorithm *)
+(**********************************************************************)
+
+(*** We define (pseudo-)divergence from Ackermann function ***)
+
+Definition ack (n : nat) :=
+ (fix F (n0 : nat) : nat -> nat :=
+ match n0 with
+ | O => S
+ | S n1 =>
+ fun m : nat =>
+ (fix F0 (n2 : nat) : nat :=
+ match n2 with
+ | O => F n1 1
+ | S n3 => F n1 (F0 n3)
+ end) m
+ end) n.
+
+Notation OMEGA := (ack 4 4).
+
+Definition f (x:nat) := x.
+
+(* Evaluation in tactics can somehow be controlled *)
+Lemma l1 : OMEGA = OMEGA.
+reflexivity. (* succeed: identity *)
+Qed. (* succeed: identity *)
+
+Lemma l2 : OMEGA = f OMEGA.
+reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *)
+Abort. (* but it reduces the right side first! *)
+
+Lemma l3 : f OMEGA = OMEGA.
+reflexivity. (* succeed: reduce left side first *)
+Qed. (* succeed: expected concl (the one with f) is on the left *)
+
+Lemma l4 : OMEGA = OMEGA.
+assert (f OMEGA = OMEGA) by reflexivity. (* succeed *)
+unfold f in H. (* succeed: no type-checking *)
+exact H. (* succeed: identity *)
+Qed. (* fail: "f" is on the left *)
+
+(* This example would fail whatever the preferred side is *)
+Lemma l5 : OMEGA = f OMEGA.
+unfold f.
+assert (f OMEGA = OMEGA) by reflexivity.
+unfold f in H.
+exact H.
+Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *)
+
+(**********************************************************************)
+(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *)
+(* (proof of span_ind_uninject_prop *)
+
+In the proof, a problem of the form (Equal S t1 t2)
+is "simpl"ified, then "red"uced to (Equal S' t1 t1)
+where the new t1's are surrounded by invisible coercions.
+A reflexivity steps conclude the proof.
+
+The trick is that Equal projects the equality in the setoid S, and
+that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)).
+
+At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1)
+and the algorithm is to first compare S and S', and t1 and t2.
+Unfortunately it does not work, and since t1 and t2 involve concrete
+instances of algebraic structures, it takes a lot of time to realize that
+it is not convertible.
+
+The only hope to improve this problem is to observe that S' hides
+(behind two indirections) a Setoid constructor. This could be the
+argument to solve the problem.
+
+