The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Dear Suneel (and list),

Instead of using Nat.ltb here, which returns a non-informative boolean, you can use

  if Compare_dec.lt_dec h 5 then ... else ...

which enriches the goal with the information (h < 5) and ~(h < 5). Then

  PeanoNat.Nat.ltb_nlt

(which I found with (Search "ltb".)) gives a translation between both notions of comparison.

Best

On Sat, Aug 14, 2021 at 1:37 PM Suneel Sarswat <suneel.sarswat AT gmail.com> 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