How do I call (p : Prop) when defining Decidable p?

Stream: Is there code for X?

[Hyunsang Hwang]

I am trying to manually define lexicographic order on Dfinsupp. Right now I am trying to prove that the lexicographic order I defined is Decidable:

import Mathlib

lemma NonzeroNonemptysupport (t : (Π₀ x : ℕ, ℕ))(nonzero : ¬t = 0) : Finset.Nonempty t.support:= by
  by_contra h
  rw [Finset.not_nonempty_iff_eq_empty, Dfinsupp.support_eq_empty] at h
  rw [<-not_iff_false_intro h]
  exact nonzero

instance lexdecidable (a b : Π₀ x : ℕ, ℕ) : Decidable (a=b ∨ (∃ i, (∀ (j : ℕ), Nat.lt j i → a j = b j) ∧ a i < b i)):=
  if sub1 : a-b=0 then isTrue _ else
    if sub2 : b-a=0 then isFalse _ else
      if List.map (b-a) (List.range ((Finset.max' (b-a).support (NonzeroNonemptysupport (b-a) sub2))+1)) >
      List.map (a-b) (List.range ((Finset.max' (a-b).support (NonzeroNonemptysupport (a-b) sub1))+1)) then
      isTrue _ else isFalse _

I want to have the proposition (∃ i, (∀ (j : ℕ), Nat.lt j i → a j = b j) ∧ a i < b i) in place of _ but I am not sure how to achieve this. Can I get some help?

[Hyunsang Hwang]

Sorry I think I have found the answer:

import Mathlib

lemma NonzeroNonemptysupport (t : (Π₀ x : ℕ, ℕ))(nonzero : ¬t = 0) : Finset.Nonempty t.support:= by
  by_contra h
  rw [Finset.not_nonempty_iff_eq_empty, Dfinsupp.support_eq_empty] at h
  rw [<-not_iff_false_intro h]
  exact nonzero

lemma tool1 (a b : Π₀ x : ℕ, ℕ) (sub1 : a-b=0) : a=b ∨ (∃ i, (∀ (j : ℕ), Nat.lt j i → a j = b j) ∧ a i < b i):=by
  sorry

lemma tool2 (a b : Π₀ x : ℕ, ℕ) (sub1 : ¬a-b=0) (sub2 : b-a=0) : ¬(a=b ∨ (∃ i, (∀ (j : ℕ), Nat.lt j i → a j = b j) ∧ a i < b i)):=by
  sorry

lemma tool3 (a b : Π₀ x : ℕ, ℕ) (sub1 : ¬a-b=0)(sub2 : ¬b-a=0)
(sub3 : List.map (b-a) (List.range ((Finset.max' (b-a).support (NonzeroNonemptysupport (b-a) sub2))+1)) >
List.map (a-b) (List.range ((Finset.max' (a-b).support (NonzeroNonemptysupport (a-b) sub1))+1)))
 : a=b ∨ (∃ i, (∀ (j : ℕ), Nat.lt j i → a j = b j) ∧ a i < b i):=by
  sorry

lemma tool4 (a b : Π₀ x : ℕ, ℕ) (sub1 : ¬a-b=0)(sub2 : ¬b-a=0)
(sub3 : ¬(List.map (b-a) (List.range ((Finset.max' (b-a).support (NonzeroNonemptysupport (b-a) sub2))+1)) >
List.map (a-b) (List.range ((Finset.max' (a-b).support (NonzeroNonemptysupport (a-b) sub1))+1))))
 : ¬(a=b ∨ (∃ i, (∀ (j : ℕ), Nat.lt j i → a j = b j) ∧ a i < b i)):=by
  sorry

instance lexdecidable (a b : Π₀ x : ℕ, ℕ) : Decidable (a=b ∨ (∃ i, (∀ (j : ℕ), Nat.lt j i → a j = b j) ∧ a i < b i)):=
  if sub1 : a-b=0 then isTrue (tool1 a b sub1) else
    if sub2 : b-a=0 then isFalse (tool2 a b sub1 sub2) else
      if sub3 : List.map (b-a) (List.range ((Finset.max' (b-a).support (NonzeroNonemptysupport (b-a) sub2))+1)) >
      List.map (a-b) (List.range ((Finset.max' (a-b).support (NonzeroNonemptysupport (a-b) sub1))+1)) then
      isTrue (tool3 a b sub1 sub2 sub3) else isFalse (tool4 a b sub1 sub2 sub3)

[Notification Bot]

Hyunsang Hwang has marked this topic as resolved.

[Notification Bot]

Bulhwi Cha has marked this topic as unresolved.