The Coq mailing list

[Julien Forest <julien.forest AT ensiie.fr>]

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
> 
> 
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  
>  [...]  

Require Import Init.Byte.
Require Import Recdef.

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

Lemma some_lemma : forall b, is_valid b = true -> b = x00 \/ b = xff.
Proof.
  intro b;functional induction (is_valid b).
  - intros _;left;reflexivity.
  - intros _;right;reflexivity.
  - discriminate.
Qed.


(* If you want to recover decidability of validity you still can
   (here by hand, or you can use some ssr stuff for decidable properties) *)
Definition valid_checker (b:byte) : { v:bool | v=true <-> is_valid b = true}.
Proof.
  functional induction (is_valid b).
  1,2: exists true;tauto.
  1: exists false;tauto.
Defined.