Zulip Chat Archive

Stream: new members

Topic: Using one Exists to prove another?

view this post on Zulip ROCKY KAMEN-RUBIO (Apr 10 2020 at 04:50):

This came up in my attempt at the first codewars Lean problem. I want to show that the inductive definition for divisibility by 3 (mult_3) implies that the number can also be written as a multiple of 3. I'm getting stuck at the end of my p_eq_3n proof. I want to extract a k from h, and then use k+3 on my goal state, and I saw another post suggest using classical.some, but then my goal state doesn't seem responsive to rfl. Am I misusing classical.some? Is there another way to do this?

import data.nat.basic
import data.set

open nat

inductive mult_3 : set 
| mult_3_O :
    mult_3 0
| mult_3_SSS :  n,
    mult_3 n 
    mult_3 (n + 3)

open_locale classical
lemma p_eq_3n (n : ) : mult_3 n   (k:), n = 3*k :=
intro hn,
apply mult_3.rec_on hn,
apply exists.intro 0,
intros n hn2 h,
have k := classical.some h,
apply exists.intro (k + 1),

view this post on Zulip Kenny Lau (Apr 10 2020 at 04:52):

cases h with k hk,

view this post on Zulip ROCKY KAMEN-RUBIO (Apr 10 2020 at 05:14):

Kenny Lau said:

cases h with k hk,

Thank you!

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 05:35):

@ROCKY KAMEN-RUBIO Welcome to Codewars! :tada: :smile:

Last updated: May 06 2021 at 22:13 UTC