Zulip Chat Archive

Stream: new members

Topic: how to turn goal into a hypothesis automatically


view this post on Zulip Ben Nale (Sep 10 2020 at 03:11):

Hi. I want to turn my goals into hypotheses so that when I prove them I could use them later - im doing induction.
I could do a have with the goal contents but actually I want to write a repeat loop.

view this post on Zulip Johan Commelin (Sep 10 2020 at 03:17):

Hi Ben, welcome! Could you please give some example code (format it with #backticks)?

view this post on Zulip Johan Commelin (Sep 10 2020 at 03:17):

It's not so clear to me what you want exactly. If you use induction n with n IH, as tactic, then it will automatically put an induction hypothesis in your goal state.

view this post on Zulip Ben Nale (Sep 10 2020 at 03:25):

Im typing my code :)

view this post on Zulip Ben Nale (Sep 10 2020 at 03:28):

def com:    
| 0 := 1
| 1:= 3
| (n+2) := com (n+1) + 2*com(n)

lemma com_7 (k: ):com(6*k)%7 =1  com(6*k+1) %7 =3  com(6*k+2) %7 =5  com(6*k+3) %7=4  com(6*k+4) %7 = 0  com(6*k+5) %7=1 :=
begin
induction k with d hd,
simp, omega,
rcases hd with  h1,h2,h3,h4,h5,h6 ,
end

view this post on Zulip Ben Nale (Sep 10 2020 at 03:31):

the proof i am trying to implement is that com mod 7 is basically
1 3 5 4 0 1 and the pattern repeats

view this post on Zulip Ben Nale (Sep 10 2020 at 03:44):

Actually, I've found a way to do it with 2step induction. Thanks for your help :)


Last updated: May 18 2021 at 17:44 UTC