The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 02 Dec 2012 21:42:56 -0800,
S3 
<scubed2 AT gmail.com>
 a écrit :

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
> 
> (*
> Rewrite doesn't match, even though the forms look the same.
> Why isn't it accepted?  How do they differ?
> I tried "Set Printing All", but that didn't reveal any
> hidden Set vs. Type differences.
> I'm using Coq 8.3pl1 (July 2011).
> *)

The problem, is that Coq is not smart enough to guess the correct
typing.

That sequence of tactics work at the point where you do your "change …"

  set (a0 := (fun _ : positive => A)
          : positive -> Type).
  set (a1 := (f a)
          : a0 xH).
  set (a2 := (fun (_ : positive) IHp => f IHp)
          : forall p, a0 p -> a0 (Pos.succ p)).
  set (a3 := Ppred (xI p)
          : positive).
  change (Repeat (xI p) f a = a2 a3 (Prect a0 a1 a2 a3)).
  rewrite <- Prect_succ.

But if you remove the type annotations of each of the "set …", it does
not work anymore (same thing with your "let a… := … in …", just add
the type anotations matching Prect_succ, and it works).

Not all type anotations are required of course (for instance that one
of a3, or that one of a0), but Coq naturally gives "A" for the type of
a1 and not "a0 xH" as you would like, so it does not match the
expected type for Prect_succ and application reports an error.

Type inferrence is not decidable in general, but in that case, I guess
tactics could do a better work to guess them.

Alternatively, if you do not wish to give all these type anotations,
you can do something like:

  exact (Prect_succ (fun _ => A) (f a) (fun _ IHp => f IHp)
                    (Ppred (p~1))).

Instead of all your stuff (shorter to write, and more efficient).
In fact with what you do, it is as if you were in the following
situation:

a : A
b : B
H : a = b
===========
a = b

and you were doing "rewrite H; reflexivity."
it works, but here "assumption." is way better from my point of view.


> 
> Require Import ZArith.
> 
> (* Iteratively call a function on itself p times. *)
> Definition Repeat {A} (p : positive) (f : A -> A) (a : A) : A :=
>   Prect (fun _ => A) (f a) (fun _ IHp => f IHp) p
> .
> 
> (*
> Theorem Repeat_eq A p f (a : A) : Repeat p f a =
>   match p with
>   | xH => f a
>   | _ => f (Repeat (Ppred p) f a)
>   end
> .
>   destruct p.
>       change (Repeat p~1 f a =
>         (let a0 := fun _ => A in
>          let a1 := f a in
>          let a2 := fun _ IHp => f IHp in
>          let a3 := Ppred p~1 in
>          a2 a3 (Prect a0 a1 a2 a3))).
>       rewrite <- Prect_succ.
> 
> > rewrite <- Prect_succ. ^^^^^^^^^^^^^^^^^^^^^
> Error:
> Found no subterm matching "?72 ?73 (Prect ?70 ?71 ?72 ?73)" in the
> current goal. *)
> 
> - -- 
> echo 'scale=2735;sqrt(57)' | BC_LINE_LENGTH=391 bc |
> tail -n 1 | tr 0-9 'ertiSSngl '
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v2.0.19 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://www.enigmail.net/
> 
> iEYEARECAAYFAlC8O+AACgkQxzVgPqtIcftqOgCfeF408hFKa9Qo0vfyGog0/5j0
> FR4Anj7/Sg83FXVa2YlAPuchahloAxUe
> =0KRL
> -----END PGP SIGNATURE-----