The Coq mailing list

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

Here is another example of a similar problem.

Require Import Lists.List ssrbool.

Fixpoint memb (a:nat)(ell: list nat){struct ell}: bool:=
match ell with
| nil =>false
| a1::ell1 => (Nat.eqb a a1) || memb a ell1
end.

Record r:=mkr { x: nat; xc: Nat.ltb x 5 = false}.

Definition gt5 (ell: list nat)(x:nat):= if (memb x ell) then 6 else 0.

Fixpoint f (ell:list nat):(list r).
refine( match ell with
|nil => nil
|h::ell' => if (memb h ell') then f ell' else (mkr (gt5 ell h) _)::f ell'

end). 

Thanks,

Suneel

On Sat, Aug 14, 2021 at 6:44 PM Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:

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