The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Thanks for suggesting the handy fix and the minimal example. I will submit a bug report.

By the way, is there a way to use the refine tactic with the Function command so that complex functions with proofs can be written in a simple way?

On Wed, Aug 12, 2020 at 2:11 AM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi,

> Is this a known issue with a simple workaround?

I did not test in your precise example but a simple workaround should
be to give a name to the class arguments, as in:

  Function toInc (f : trace indA -> trace indB) `{tf : TraceFunction f} `{mf : Monotone f}
  (ins : list (trace indA)) {measure length ins} : (list (trace indB)) :=
  match (rev ins) with
  | [] => [f []]
  | (new :: inss) =>
    let insofar := (concat (rev inss)) in
    (toInc f (rev inss))
      ++ [proj1_sig (monotonicity_witness insofar (insofar ++ new)
         (exist _ new (reflexivity (insofar ++ new))))]
  end.

Don't hesitate to submit a bug report at github.com/coq/coq/issues so
that it is recorded. Indeed, the fix should be easy (Function was
written at a time when type classes where not yet available and under
the invariant - changed by type classes - that all arguments had
names).

Best,

Hugo

--------------------------------------------------------------------------------
In case it is useful, here is a short example showing the same problem:

Require Import Recdef.
Class Bar.
Function iszero (n : nat) `{Bar} {measure id n} : bool :=
  match n with
  | O => true
  | _ => false
  end.

On Tue, Aug 11, 2020 at 09:02:02PM -0500, Agnishom Chattopadhyay wrote:
> Hi;
>
> When I try to run the command in line 516 here, I get a strange error:
>
>
> Function toInc (f : trace indA -> trace indB) `{TraceFunction f} `{Monotone f}
> (ins : list (trace indA))
>
> {measure length ins} : (list (trace indB)) :=
>
> match (rev ins) with
>
> | [] => [f []]
>
> | (new :: inss) =>
>
> let insofar := (concat (rev inss)) in
>
> (toInc f (rev inss))
>
> ++ [proj1_sig (monotonicity_witness insofar (insofar ++ new)
>
> (exist _ new (reflexivity (insofar ++ new))))]
>
> end.
>
>
>
> (* Error: Anomaly "File "plugins/funind/gen_principle.ml", line 1526,
> characters 37-43: Assertion failed."
>
> Please report at http://coq.inria.fr/bugs/.
>
> *)
>
> Is this a known issue with a simple workaround? I tried using `Program Fixpoint
> ` instead, but sadly Program Fixpoint does not generate an equation and creates
> a term very difficult to work with.