Stream: Coq users

Topic: use of induction tactic

view this post on Zulip pianke (Mar 28 2023 at 17:43):

l have natural number list l1 then pass it as input argument to function z(l1 l2 l3) (bool output). After applying induction first time l1 becomes l1=[c0::t]. In H1: [c0::t] <>nil->
if eqlist l2 l3 then z(l1 l2 l3)=true else false...
After applying induction second time l1=[c0::c1::t]. then get H2.But this process never ends.I want to ask may i use H1 in H2? What to do? I am applying induction on l1 then empty case get easily resolve but in second case i am testing the conditions on new elements [c0::c1::c2....]

view this post on Zulip Laurent Théry (Mar 28 2023 at 17:50):

can you give exact coq code?

Last updated: Oct 04 2023 at 20:01 UTC