Ssreflect Users Discussion List

[sidi <>]

Hi Vincent,

I think you may have encounter a bug, bcz the term u get in you goal is clearly ill typed or maybe Coq is doing some magic in the background. When I do a set h' := (Logic.eq_refl true) Coq said that the acc_gcd ... is ill typed!

A temporary solution to you proof is to do the standard induction on r, this will prevent Coq from doing too much simplification in the goal and u will have instead of (Logic.eq_refl true) a (Logic.eq_refl (0 < r.+1)).

case: r h1 h2 => /= [| r] h1 h2; rewrite h1.
  by case Dgb: (g %| b) => /=; rewrite 1?andbF 1?addn0 1?dvdn_mull.
set h' := (Logic.eq_refl (0 < r.+1)).
rewrite (hi r.+1 (h2 hb) b (h2 hb) h' g).
by case Dgb: (g %| b) => /=; rewrite 1?andbF 1?andbT // dvdn_addr 1?dvdn_mull.
Qed.

Regards.

On Tue, May 10, 2011 at 10:24 PM, Vincent Siles <> wrote:

Hi there,
We have a problem trying to do a proof with a dependent induction scheme.
we want to compute the gcd of two nats, and prove it correct, by
well-founded induction
on < .
We managed to write the function, but there is a weird behavior of
rewrite during
the proof of correctness (a complete file is attached to the email).

At some point, we have the following goal
  (g %| (if 0 < r as b0 return (protect_term ((0 < r) = b0) -> nat)
       then [eta acc_gcd (hA r (h2 hb)) (h2 hb)]
       else fun _ : (0 < r) = false => b) (Logic.eq_refl (0 < r))) =
  (g %| a) && (g %| b)
and we need to perform a case analysis on (0 < r). After doing so, the goal is

  (g %| acc_gcd (hA r (h2 hb)) (h2 hb) (Logic.eq_refl true)) =
  (g %| a) && (g %| b)

The problem is that (Logic.eq_refl (0 < r)) is now (Logic.eq_refl true) which
ends to be ill-typed (I'm not completely sure about this point). At this
point, if we try to use the induction hypothesis for example, we get:

Toplevel input, characters 0-37:
Error: Refiner was given an argument "Logic.eq_refl true" of type
 "true = true" instead of "is_true (0 < r)".

Is there a way to prevent this instance of (0 < r) to be rewritten ?

Cheers,
Vincent

-- 
Sidi