The Coq mailing list

[Blaudeau Clément <clement.blaudeau AT kes.eleves.polytechnique.fr>]

Thank you for your answer !

I’ve tried to use Function, but Coq cannot create the inductive predicate R_is_valid as soon as I add the non-trivial cases :

is_valid is defined
is_valid is recursively defined (decreasing on 1st argument)
Warning: Cannot define graph(s) for is_valid [funind-cannot-define-graph,funind]
Warning: Cannot build inversion information [funind-cannot-build-inversion,funind

However, to me, my function looks like a valid pattern matching tree without dependent type (the two issues mentioned in the documentation). The cases that are not accepted by Coq are of the following form :

| N b1 (((N b2 _ ) as d2)::((N b3 _) as d3)::nil) => (* sequence of boolean tests *) && (is_valid d2) && (is_valid d3)

Am I missing something ?

Thank you again,

Best,

Clément

Le 29/06/2020 à 20:29, Julien Forest a écrit :

On Mon, 29 Jun 2020 18:08:34 +0200
Xavier Leroy <xavier.leroy AT college-de-france.fr> wrote:

On Mon, Jun 29, 2020 at 5:39 PM Gaëtan Gilbert <
 [...]  

 [...]  

That's a very good trick, and it can be automated using Function
instead of Definition, see ttps://
coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#coq:cmd.function

Function is_valid b :=
  match b with
  | x00 | xff => true
  | _ => false (* 254 cases hidden in this _ *)
  end.

will generate the inductive predicate R_is_valid and the proofs of
equivalence with the is_valid function.

Hope this helps,

- Xavier Leroy

Just to illustrate both Gaëtan and Xavier ideas using Function.

Cheers, 

Julien Forest

 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  

      ​