Imported Upstream version 8.8.2upstream/8.8.2

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.
+
+