a = c \/ False ->
a = d \/ False ->
g_value x y z (a::l1)=true
First , what is the meaning of above?
Secondly, I have two functions whose input arguments are (nat &list nat) and output is bool.Both functions gives true only when list length is greater than 3. To write lemma statement i should add constraint of length>3?
You should be able to prove c = d \/ False
equivalent to c = d
.
Could you upload a paste of your file to get an understanding what you're trying to do?
I have simplified above . Now this is the case where one constructor give following
Fixpoint g (x y z: nat) ( l : list nat) : bool :=
match z with
|0=> false
|S n' => match l with
| nil => false
| [a] =>if (eqb x y && eqb x a) then true else false
...
g x y (S z) [a] = true ->
eqb x y =true. To prove this I should apply induction so that discuss cases one by one. When i simplify g i get match g with o |Sn'. Although i have ( S z) in hypothesis. Now what to do?
This should work:
Goal forall x y z a, g x y (S z) [a] = true -> eqb x y = true.
intros x y z a; simpl; case (eqb x y); [trivial | discriminate].
Qed.
You sent an incomplete definition of g
(using ...
dots). I don't think it's up to us to guess missing parts of code.
Last updated: Oct 13 2024 at 01:02 UTC