## Stream: Coq users

### Topic: extract information

#### sara lee (Feb 17 2023 at 18:03):

``````H:  true &&
match t with
| [] => false
| b :: t =>
if f b c
then
determin z1 z2  n l b t
(fur q s values)
else false
end = true

goal: true &&
(if f b c
then
determin z1 z2  n l b t
(fur q s values)
else false) = true
``````

I have hypothesis and goal more or less in same form. How i can use H in solving goal statement? In present situation first command i should apply is induction t in H (am i right?)
If i do this , then induction t as [ | b' t1].

``````H1: determin z1 z2  n l b' t1
(fur q s values)= true

goal: determin z1 z2  n l b  tl'
(fur q s values)= true
``````

still i can't use H1. How to come out?

#### Li-yao (Feb 17 2023 at 19:02):

in `H`, the first `t` is shadowed by its tail. So these assumptions really mean something different.

#### sara lee (Feb 19 2023 at 17:37):

I have simplified/modified above . Output of fur (value s k (d:: l)) is list nat. q s c are nat.
H:=In c l
goal: match fur (value s q (d:: l)) with
| [] => false
Now again this is false due to the occurence of d & c. I have applied destruct command on fur (value s k (d:: l)) then get false=true. To avoid this i should have inversion . May i write it as In c l -> In c [] -> False. When i will apply it then from where i bring In c [] . (or some other way)

#### Laurent Théry (Feb 19 2023 at 19:24):

Maybe you need to keed track of the value of `fur` to finish the proof

``````destruct (fur (value s q (d :: l))) as [|x xl] eqn : Heq.
``````

Last updated: Jun 23 2024 at 23:01 UTC