Stream: Coq users

Topic: conditions

zohaze (Mar 11 2023 at 15:50):

H1 : f4 a b 0  [] = true
Fixpoint f4 (a b c : nat) ( l  : list nat) : bool :=
  match c with
|0=> false
|S n=> match l with
     |nil =>false
     |h::t=>...

f4 gives false in case c=0 & l=[]. But i have hypothesis that it gives true . I want to write left side of f4=false so that
it become false=true. I simply unfold f4 then

get message fix f4
(a b c : nat) (l : list nat) : bool :=
match c with
|0=>false
|S _=>
Why this happening when i already destruct c?

Last updated: Oct 04 2023 at 20:01 UTC