The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

Thanks Gaëtan,

This worked for me but now unfolding and rewriting involving f is difficult to deal with!

I guess I should follow the book by Adam to hope to get what I am looking for.

Thanks again.

Regards,

Suneel

On Sat, Aug 14, 2021 at 7:32 PM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

With tactics you can do

Fixpoint f (ell:list nat):(list r).
Proof.
   refine (match ell with
           | nil => nil
           | cons h ell' => _
           end).
   destruct (Nat.ltb h 5) eqn:H.
   - exact (f ell').
   - exact (cons (mkr h H) (f ell')).
Defined.

With a direct term:

Fixpoint f (ell:list nat) : list r :=
   match ell with
   | nil => nil
   | cons h ell' =>
     (if Nat.ltb h 5 as b return Nat.ltb h 5 = b -> list r
      then fun _ => f ell'
      else fun H => cons (mkr h H) (f ell'))
       eq_refl
   end.

Gaëtan Gilbert

On 14/08/2021 13:36, Suneel Sarswat wrote:
> I have a simple problem. I can't find any web link/document for this kind of situation. I have a record type r as
> * Record r:=mkr { x: nat; xc: Nat.ltb x 5 = false}.*
> Now I want to write a function which takes a list ell of natural numbers and returns a list of type r as
> *Fixpoint f (ell:list nat):(list r).
>   refine ( match ell with
>    |nil => nil
>    |h::ell' => if Nat.ltb h 5 then f ell' else (mkr h _)::f ell'
> end ).*
> The problem is it gives me a goal to prove "Nat.ltb h 5 = false" without the branch information or any condition on term h. In general how to extract branch information/pass dependent proof terms in a specific branch of function?
> Thanks in advance.
> Regards,
> Suneel