## Stream: Coq users

### Topic: meaning of statement

#### sara lee (Mar 11 2023 at 18:10):

``````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?

#### James Wood (Mar 11 2023 at 18:20):

You should be able to prove `c = d \/ False` equivalent to `c = d`.

#### Stefan Haan (Mar 12 2023 at 06:12):

Could you upload a paste of your file to get an understanding what you're trying to do?

#### sara lee (Mar 12 2023 at 08:45):

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?

#### Pierre Castéran (Mar 12 2023 at 18:05):

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 04 2023 at 20:01 UTC