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: Oct 13 2024 at 01:02 UTC