Stream: Coq users

Topic: meaning of statement

view this post on Zulip 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?

view this post on Zulip James Wood (Mar 11 2023 at 18:20):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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].

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