The Coq mailing list

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

Thanks Gabriel, however it does not answer my question.

I am looking for a more general anwer, i.e., how to carry branch information during the proof. 

I am sorry if the example I created does not convey this. In my problem: for example, in one of the branches I have a condition that if 'h' belongs to 'ell' then 'O', where 'O' carries a hole and 

to prove the hole I need 'h' belongs to 'ell' in my hypothesis. Your answer is for a specific situation of comparison of numbers.

Let me know if a more elaborate example is needed if I am not making any sense. 

Regards,

Suneel

On Sat, Aug 14, 2021 at 6:09 PM Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

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