The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

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