another confusing type mismatch

Stream: lean4

[Jared green]

i dont know how to resolve this
(im still on 4.9.0-rc3)

i get a type mismatch at the end of case h.right.right.a.a of op2(before the sorry) the proof is otherwise complete.

something about instDecidableEqProd a b vs propDecidable (a = b) which probably shouldnt even be there.

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

@[reducible]
def interl (l : List (List a)) [DecidableEq a] : List a :=
  match l with
  | [] => []
  | a :: [] => a
  | (a :: as) => List.inter a (interl as)

theorem interl_all (s : a -> Prop) : ∀ l : List (List a),
          l.any (fun x => x.all (fun y => s y)) -> ∀ b ∈ interl l, s b :=
  by
  intro l
  simp
  induction' l with hd t ht
  simp
  simp
  constructor
  intro hx
  unfold interl
  cases' Classical.em (t = []) with hht hnt
  rw [hht]
  simp
  exact hx
  simp
  apply List.forall_mem_inter_of_forall_left
  exact hx
  unfold interl
  cases' Classical.em (t = []) with hht hnt
  rw [hht]
  simp
  simp
  intro x hx hhx
  apply List.forall_mem_inter_of_forall_right
  apply ht
  exact hx
  exact hhx

theorem interl_all_filter (s : a -> Prop)(t : List a -> Prop) : (∀ x : List a, ¬ t x -> ¬(x.all fun y => s y))
     -> ∀ l : List (List a), (l.any (fun x => x.all (fun y => s y))
     -> ∀ b ∈ interl (l.filter (fun x => t x)), s b) :=
  by
  intro ha l hl
  simp at hl
  obtain ⟨ m, hm, hhm⟩ := hl
  induction' l with hd tl ht
  simp
  rw [List.filter_cons]
  cases' Classical.em (t hd) with htll htlr
  apply eq_true at htll
  rw [htll]
  simp
  cases' Classical.em (tl = []) with htl htr
  rw [htl]
  simp
  have hmd : m = hd := by
  {
    simp at hm
    cases' hm with hml hmr
    assumption
    exfalso
    rw [htl] at hmr
    apply List.not_mem_nil at hmr
    exact hmr
  }
  rw [← hmd]
  exact hhm
  cases' Classical.em (List.filter (fun x ↦ decide (t x)) tl = []) with htn htf
  have hdm : interl (hd :: List.filter (fun x ↦ decide (t x)) tl) = hd := by {
    rw [htn]
  }
 rw [hdm]
  simp at hm
  cases' hm with hm hm
  rw [← hm]
  exact hhm
  exfalso
  rw [List.filter_eq_nil] at htn
  apply htn at hm
  apply ha
  simp at hm
  exact hm
  simp
  exact hhm
  unfold interl
  simp
  cases' Classical.em (m ∈ tl) with hmt hhd
  apply List.forall_mem_inter_of_forall_right
  apply ht
  exact hmt
  apply List.forall_mem_inter_of_forall_left
  have hmd : m = hd := by{
    simp at hm
    cases hm
    assumption
    exfalso
    apply hhd
    assumption
  }
  rw [← hmd]
  exact hhm
  have hmnt : m ≠ hd := by {
    intro hmt
    apply ha
    exact htlr
    simp
    rw [← hmt]
    exact hhm
  }
  apply eq_false at htlr
  rw [htlr]
  simp
  cases' Classical.em (tl = []) with htl htr
  rw [htl]
  simp
  simp at hm
  cases hm
  exfalso
  apply hmnt
  assumption
  apply ht
  assumption

theorem forall_mem_or {b : α -> Prop}{c : α -> Prop}{e : α -> Prop}: (∀ a, (b a ∨ c a) -> e a) <-> (∀ a, b a -> e a) ∧ (∀ a, c a -> e a ) :=
  by
  constructor
  intro ha
  constructor
  intros a hha
  apply ha
  left
  exact hha
  intros a hha
  apply ha
  right
  exact hha
  intro ha
  intros a hha
  obtain ⟨ hal, har ⟩ := ha
  cases hha
  apply hal
  assumption
  apply har
  assumption

theorem interl_filter_filter (d : a -> Prop)(e : List a -> Prop):
        ∀ b : a,∀ c : List (List a),
        b ∈ interl ((c.filter (fun x: List a => e x)).map (fun x => x.filter (fun y : a => (d y) )))
        -> b ∈ interl (c.filter fun x => e x) :=
  by
  intro f
  intro l
  induction' l with hd t ht
  simp
  cases' Classical.em (e hd) with hdl hdr
  intro hi
  rw [List.filter_cons]
  simp
  apply eq_true at hdl
  rw [hdl]
  simp
  rw [List.filter_cons] at hi
  rw [hdl] at hi
  simp at hi
  cases' Classical.em (  (List.filter (fun x ↦ decide (e x)) t) = []) with hfe hff
  unfold interl
  rw [hfe]
  simp
  unfold interl at hi
  rw [hfe] at hi
  simp at hi
  apply List.filter_subset at hi
  exact hi
  unfold interl
  simp
  have hhi : f ∈
    (List.filter (fun y ↦ decide (d y)) hd).inter
    (interl (List.map (fun x ↦ List.filter
    (fun y ↦ decide (d y)) x) (List.filter
    (fun x ↦ decide (e x)) t))) := by{
    unfold interl at hi
    revert hi
    have hfm : List.map (fun x ↦ List.filter (fun y ↦ decide (d y)) x) (List.filter (fun x ↦ decide (e x)) t) ≠ [] := by {
      intro hg
      simp at hg
      apply hff
      exact hg
    }
    simp
  }
  apply List.mem_inter_of_mem_of_mem
  apply List.inter_subset_left at hhi
  apply List.filter_subset at hhi
  exact hhi
  apply List.inter_subset_right at hhi
  apply ht
  exact hhi
  rw [List.filter_cons]
  apply eq_false at hdr
  rw [hdr]
  simp
  exact ht

theorem op2 : ∀ n : List (List (List (Bool × normalizable α pred))),
              ∀ g h : List (List (Bool × normalizable α pred)), h ∈ n -> g.all (fun x => h.any (fun y => bcompatible x y)) ->
              nToProp n -> (gToProp g <-> gToProp (g.map (fun x => x.append (interl ((h.filter (fun y => bcompatible x y)).map
              (fun y => y.filter (fun z => z ∉ x))))))) :=
  by
  intro n g hi hhi hg hn
  simp at hg
  simp
  unfold gToProp
  simp
  constructor
  intro hl
  obtain ⟨ t,ht,hht⟩ := hl
  use t
  have h_comp_exists: ∃ y ∈ hi, bcompatible t y := by {
    apply hg
    exact ht
  }
  have hhm : (hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t) ) ≠ [] := by {
    simp
    rcases h_comp_exists with ⟨y, hy_in_hi, hy_comp_t⟩
    apply List.ne_nil_of_mem
    apply List.mem_filter_of_mem
    exact hy_in_hi
    exact hy_comp_t
  }
  constructor
  exact ht
  unfold sToProp
  rw [all_and]
  constructor
  unfold sToProp at hht
  simp only [List.all_eq_true, decide_eq_true_eq]
  simp only [List.all_eq_true, decide_eq_true_eq] at hht
  exact hht
  unfold nToProp at hn
  simp only [List.all_eq_true, decide_eq_true_eq] at hn
  have hgi : gToProp hi := by {
    apply hn at hi
    apply hi at hhi
    exact hhi
  }
  unfold gToProp at hgi
  unfold sToProp at hgi
  have hfi : gToProp ((hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t))) := by{
    unfold gToProp
    have hfh : gToProp (hi.filter (fun x=> bcompatible t x)) := by {
      apply any_filter_imp (fun x => bcompatible t x) (fun x => sToProp x) at hi
      unfold gToProp
      rw [← hi]
      unfold sToProp
      exact hgi
      intro x hx
      apply compatibility at hx
      simp at hx
      simp
      apply hx
      exact hht
    }
    unfold gToProp at hfh
    unfold sToProp at hfh
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hfh
    obtain ⟨ x, hx,hhx⟩ := hfh
    simp
    use x
    constructor
    exact hx
    unfold sToProp
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hgi
    apply all_filter
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool]
    exact hhx
  }
  simp only [List.all_eq_true, decide_eq_true_eq]
  intros p ho
  apply interl_all_filter wToProp (fun y => bcompatible t y)
  intro l hlb hla
  have hlaf : sToProp l := by {
    unfold sToProp
    exact hla
  }
  apply compatibility at hlb
  apply hlb
  constructor
  exact hht
  exact hlaf
  simp only [List.all_eq_true, decide_eq_true_eq, Prod.forall
  ,  Bool.decide_and, List.any_eq_true, Bool.and_eq_true] at hgi
  simp only [List.any_eq_true, List.all_eq_true, decide_eq_true_eq, Prod.forall]
  exact hgi
  apply interl_filter_filter (fun z => !(z ∈ t)) (fun x => bcompatible t x)
  simp
  --exact ho  --for some reason this is a type mismatch
  sorry
  intro hr
  unfold sToProp at hr
  unfold sToProp
  simp only [List.all_eq_true, decide_eq_true_eq]
  simp only [List.all_eq_true, List.mem_append, decide_eq_true_eq, ] at hr
  obtain ⟨ a, ha, hag⟩ := hr
  rw [forall_mem_or] at hag
  obtain ⟨ hagl,hagr⟩ := hag
  use a

[Alex J. Best]

Your code doesnt work in the web editor, it complains that it doesnt know what toProp is (and several other things)

[Jared green]

place this after namespace normalizable:

@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl

[Jared green]

and this:

@[reducible]
def nStrip (n : normalizable α pred) : Bool × normalizable α pred :=
  match n with
  | Not i => (false,i)
  | i => (true,i)

[Jared green]

(in that order)

[Jared green]

and this also:

def bcompatible (s : List (Bool × normalizable α pred)) (t : List (Bool × normalizable α pred)) : Bool :=
  s.all (fun x => t.all (fun y =>  x.snd == y.snd -> x.fst == y.fst))

theorem compatibility :∀ a b : List (Bool × normalizable α pred),  (¬ bcompatible a b = true) -> ¬(sToProp a ∧ sToProp b) :=
  by
  intro a b hb hab
  unfold bcompatible at hb
  simp only [beq_iff_eq, List.all_eq_true, decide_eq_true_eq, Bool.forall_bool,
    implies_true, imp_false, true_and, and_true, not_and, not_forall, not_not, exists_prop,
    exists_eq_right'] at hb
  obtain ⟨ y,hy,z,hz,hyzl,hyzr⟩ := hb
  obtain ⟨ hsa,hsb⟩ := hab
  have hyw : wToProp y := by {
    unfold sToProp at hsa
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool] at hsa
    apply hsa
    exact hy
  }
  have hzw : wToProp z := by {
    unfold sToProp at hsb
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool] at hsb
    apply hsb
    exact hz
  }
  have hy1 : y.1 == ! z.1 := by {
    simp
    cases' Classical.em (y.1 = true) with hy hy
    cases' Classical.em (z.1 = true) with hz hz
    by_contra hzy
    simp at hzy
    apply hyzr
    exact hzy
    simp at hz
    rw [hz]
    simp
    rw [hy]
    cases' Classical.em (z.1 = true) with hz hz
    simp at hy
    rw [hz]
    rw [hy]
    simp
    rw [eq_comm]
    by_contra hyz
    simp at hyz
    apply hyzr
    rw [eq_comm]
    exact hyz
  }
  simp at hy1
  have hyp : y = (y.1,y.2) := by {
    simp
  }
  rw [hyp] at hyw
  rw [hy1] at hyw
  rw [hyzl] at hyw
  rw [w_neg] at hyw
  apply hyw
  exact hzw

[Damiano Testa]

Could you paste a single code-block that can be opened in the online server and "just works"? If it can be an approximation of a #mwe, even better! But just something that can be viewed with a click will already be very useful to whoever feels like helping you!

[Jared green]

itis unfortunately too long so here is the first part:

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable
@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl

@[reducible]
def nStrip (n : normalizable α pred) : Bool × normalizable α pred :=
  match n with
  | Not i => (false,i)
  | i => (true,i)

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

def bcompatible (s : List (Bool × normalizable α pred)) (t : List (Bool × normalizable α pred)) : Bool :=
  s.all (fun x => t.all (fun y =>  x.snd == y.snd -> x.fst == y.fst))

theorem compatibility :∀ a b : List (Bool × normalizable α pred),  (¬ bcompatible a b = true) -> ¬(sToProp a ∧ sToProp b) :=
  by
  intro a b hb hab
  unfold bcompatible at hb
  simp only [beq_iff_eq, List.all_eq_true, decide_eq_true_eq, Bool.forall_bool,
    implies_true, imp_false, true_and, and_true, not_and, not_forall, not_not, exists_prop,
    exists_eq_right'] at hb
  obtain ⟨ y,hy,z,hz,hyzl,hyzr⟩ := hb
  obtain ⟨ hsa,hsb⟩ := hab
  have hyw : wToProp y := by {
    unfold sToProp at hsa
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool] at hsa
    apply hsa
    exact hy
  }
  have hzw : wToProp z := by {
    unfold sToProp at hsb
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool] at hsb
    apply hsb
    exact hz
  }

  have hy1 : y.1 == ! z.1 := by {
    simp
    cases' Classical.em (y.1 = true) with hy hy
    cases' Classical.em (z.1 = true) with hz hz
    by_contra hzy
    simp at hzy
    apply hyzr
    exact hzy
    simp at hz
    rw [hz]
    simp
    rw [hy]
    cases' Classical.em (z.1 = true) with hz hz
    simp at hy
    rw [hz]
    rw [hy]
    simp
    rw [eq_comm]
    by_contra hyz
    simp at hyz
    apply hyzr
    rw [eq_comm]
    exact hyz
  }

  simp at hy1
  have hyp : y = (y.1,y.2) := by {
    simp
  }
  rw [hyp] at hyw
  rw [hy1] at hyw
  rw [hyzl] at hyw
  rw [w_neg] at hyw
  apply hyw
  exact hzw

@[reducible]
def interl (l : List (List a)) [DecidableEq a] : List a :=
  match l with
  | [] => []
  | a :: [] => a
  | (a :: as) => List.inter a (interl as)

theorem interl_all (s : a -> Prop) : ∀ l : List (List a),
          l.any (fun x => x.all (fun y => s y)) -> ∀ b ∈ interl l, s b :=
  by
  intro l
  simp
  induction' l with hd t ht
  simp
  simp
  constructor
  intro hx
  unfold interl
  cases' Classical.em (t = []) with hht hnt
  rw [hht]
  simp
  exact hx
  simp
  apply List.forall_mem_inter_of_forall_left
  exact hx
  unfold interl
  cases' Classical.em (t = []) with hht hnt
  rw [hht]
  simp
  simp
  intro x hx hhx
  apply List.forall_mem_inter_of_forall_right
  apply ht
  exact hx
  exact hhx

theorem interl_all_filter (s : a -> Prop)(t : List a -> Prop) : (∀ x : List a, ¬ t x -> ¬(x.all fun y => s y))
     -> ∀ l : List (List a), (l.any (fun x => x.all (fun y => s y))
     -> ∀ b ∈ interl (l.filter (fun x => t x)), s b) :=
  by
  intro ha l hl
  simp at hl
  obtain ⟨ m, hm, hhm⟩ := hl
  induction' l with hd tl ht
  simp
  rw [List.filter_cons]
  cases' Classical.em (t hd) with htll htlr
  apply eq_true at htll
  rw [htll]
  simp
  cases' Classical.em (tl = []) with htl htr
  rw [htl]
  simp
  have hmd : m = hd := by
  {
simp at hm
    cases' hm with hml hmr
    assumption
    exfalso
    rw [htl] at hmr
    apply List.not_mem_nil at hmr
    exact hmr
  }
  rw [← hmd]
  exact hhm
  cases' Classical.em (List.filter (fun x ↦ decide (t x)) tl = []) with htn htf
  have hdm : interl (hd :: List.filter (fun x ↦ decide (t x)) tl) = hd := by {
    rw [htn]
  }
rw [hdm]
  simp at hm
  cases' hm with hm hm
  rw [← hm]
  exact hhm
  exfalso
  rw [List.filter_eq_nil] at htn
  apply htn at hm
  apply ha
  simp at hm
  exact hm
  simp
  exact hhm
  unfold interl
  simp
  cases' Classical.em (m ∈ tl) with hmt hhd
  apply List.forall_mem_inter_of_forall_right
  apply ht
  exact hmt
  apply List.forall_mem_inter_of_forall_left
  have hmd : m = hd := by{
simp at hm
    cases hm
    assumption
    exfalso
    apply hhd
    assumption
  }
  rw [← hmd]
  exact hhm
  have hmnt : m ≠ hd := by {
    intro hmt
    apply ha
    exact htlr
    simp
    rw [← hmt]
    exact hhm
  }
  apply eq_false at htlr
  rw [htlr]
  simp
  cases' Classical.em (tl = []) with htl htr
  rw [htl]
  simp
  simp at hm
  cases hm
  exfalso
  apply hmnt
  assumption
  apply ht
  assumption


theorem forall_mem_or {b : α -> Prop}{c : α -> Prop}{e : α -> Prop}: (∀ a, (b a ∨ c a) -> e a) <-> (∀ a, b a -> e a) ∧ (∀ a, c a -> e a ) :=
  by
  constructor
  intro ha
  constructor
  intros a hha
  apply ha
  left
  exact hha
  intros a hha
  apply ha
  right
  exact hha
  intro ha
  intros a hha
  obtain ⟨ hal, har ⟩ := ha
  cases hha
  apply hal
  assumption
  apply har
  assumption

theorem interl_filter_filter (d : a -> Prop)(e : List a -> Prop):
        ∀ b : a,∀ c : List (List a),
        b ∈ interl ((c.filter (fun x: List a => e x)).map (fun x => x.filter (fun y : a => (d y) )))
        -> b ∈ interl (c.filter fun x => e x) :=
  by
  intro f
  intro l
  induction' l with hd t ht
  simp
  cases' Classical.em (e hd) with hdl hdr
  intro hi
  rw [List.filter_cons]
  simp
  apply eq_true at hdl
  rw [hdl]
  simp
  rw [List.filter_cons] at hi
  rw [hdl] at hi
  simp at hi
  cases' Classical.em (  (List.filter (fun x ↦ decide (e x)) t) = []) with hfe hff
  unfold interl
  rw [hfe]
  simp
  unfold interl at hi
  rw [hfe] at hi
  simp at hi
  apply List.filter_subset at hi
  exact hi
  unfold interl
  simp
  have hhi : f ∈
    (List.filter (fun y ↦ decide (d y)) hd).inter
    (interl (List.map (fun x ↦ List.filter
    (fun y ↦ decide (d y)) x) (List.filter
    (fun x ↦ decide (e x)) t))) := by{
    unfold interl at hi
    revert hi
    have hfm : List.map (fun x ↦ List.filter (fun y ↦ decide (d y)) x) (List.filter (fun x ↦ decide (e x)) t) ≠ [] := by {
      intro hg
      simp at hg
      apply hff
      exact hg
    }
    simp
  }
  apply List.mem_inter_of_mem_of_mem
  apply List.inter_subset_left at hhi
  apply List.filter_subset at hhi
  exact hhi
  apply List.inter_subset_right at hhi
  apply ht
  exact hhi
  rw [List.filter_cons]
  apply eq_false at hdr
  rw [hdr]
  simp
  exact ht

[Jared green]

and here is the rest:

theorem op2 : ∀ n : List (List (List (Bool × normalizable α pred))),
              ∀ g h : List (List (Bool × normalizable α pred)), h ∈ n -> g.all (fun x => h.any (fun y => bcompatible x y)) ->
              nToProp n -> (gToProp g <-> gToProp (g.map (fun x => x.append (interl ((h.filter (fun y => bcompatible x y)).map
              (fun y => y.filter (fun z => z ∉ x))))))) :=
  by
  intro n g hi hhi hg hn
  simp at hg
  simp
  unfold gToProp
  simp
  constructor
  intro hl
  obtain ⟨ t,ht,hht⟩ := hl
  use t
  have h_comp_exists: ∃ y ∈ hi, bcompatible t y := by {
    apply hg
    exact ht
  }
  have hhm : (hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t) ) ≠ [] := by {
    simp
    rcases h_comp_exists with ⟨y, hy_in_hi, hy_comp_t⟩
    apply List.ne_nil_of_mem
    apply List.mem_filter_of_mem
    exact hy_in_hi
    exact hy_comp_t
  }
  constructor
  exact ht
  unfold sToProp
  rw [all_and]
  constructor
  unfold sToProp at hht
  simp only [List.all_eq_true, decide_eq_true_eq]
  simp only [List.all_eq_true, decide_eq_true_eq] at hht
  exact hht
  unfold nToProp at hn
  simp only [List.all_eq_true, decide_eq_true_eq] at hn
  have hgi : gToProp hi := by {
    apply hn at hi
    apply hi at hhi
    exact hhi
  }
unfold gToProp at hgi
  unfold sToProp at hgi
  have hfi : gToProp ((hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t))) := by{
    unfold gToProp
    have hfh : gToProp (hi.filter (fun x=> bcompatible t x)) := by {
      apply any_filter_imp (fun x => bcompatible t x) (fun x => sToProp x) at hi
      unfold gToProp
      rw [← hi]
      unfold sToProp
      exact hgi
      intro x hx
      apply compatibility at hx
      simp at hx
      simp
      apply hx
      exact hht
    }
    unfold gToProp at hfh
    unfold sToProp at hfh
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hfh
    obtain ⟨ x, hx,hhx⟩ := hfh
    simp
    use x
constructor
    exact hx
    unfold sToProp
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hgi
    apply all_filter
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool]
    exact hhx
  }
  simp only [List.all_eq_true, decide_eq_true_eq]
  intros p ho
  apply interl_all_filter wToProp (fun y => bcompatible t y)
  intro l hlb hla
  have hlaf : sToProp l := by {
    unfold sToProp
    exact hla
  }
  apply compatibility at hlb
  apply hlb
  constructor
  exact hht
  exact hlaf
  simp only [List.all_eq_true, decide_eq_true_eq, Prod.forall
  ,  Bool.decide_and, List.any_eq_true, Bool.and_eq_true] at hgi
  simp only [List.any_eq_true, List.all_eq_true, decide_eq_true_eq, Prod.forall]
  exact hgi
  apply interl_filter_filter (fun z => !(z ∈ t)) (fun x => bcompatible t x)
  simp
  --exact ho  --for some reason this is a type mismatch
  sorry

[Damiano Testa]

Are the proofs of the theorems leading up to the last one really needed, or could they be replaced by sorry?

[Jared green]

you could, yes

[Jared green]

(as far as i know)

[Julian Berman]

You could was what the idea was I think :) -- the point is the easier you make it for someone to help you, the more likely it is you'll get helped typically, and making something someone can just click and see what you're trying to describe is essentially the most important step!

[Jared green]

sure.

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable
@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl

@[reducible]
def nStrip (n : normalizable α pred) : Bool × normalizable α pred :=
  match n with
  | Not i => (false,i)
  | i => (true,i)

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

def bcompatible (s : List (Bool × normalizable α pred)) (t : List (Bool × normalizable α pred)) : Bool :=
  s.all (fun x => t.all (fun y =>  x.snd == y.snd -> x.fst == y.fst))

theorem compatibility :∀ a b : List (Bool × normalizable α pred),  (¬ bcompatible a b = true) -> ¬(sToProp a ∧ sToProp b) :=
  by
  sorry

theorem any_filter_imp (s t : a -> Bool): (∀ x : a, ¬ (s x) -> ¬ (t x)) -> ∀ l : List a,l.any t <-> (l.filter s).any t :=
  by
  sorry

theorem all_and : List.all ( a ++ b) c <-> List.all a c ∧ List.all b c :=
  by
  sorry

@[reducible]
def interl (l : List (List a)) [DecidableEq a] : List a :=
  match l with
  | [] => []
  | a :: [] => a
  | (a :: as) => List.inter a (interl as)

theorem interl_all (s : a -> Prop) : ∀ l : List (List a),
          l.any (fun x => x.all (fun y => s y)) -> ∀ b ∈ interl l, s b :=
  by
  sorry

theorem all_filter (s t : a -> Bool) : ∀ l : List a, l.all s -> (l.filter t).all s :=
  by
  sorry

theorem interl_all_filter (s : a -> Prop)(t : List a -> Prop) : (∀ x : List a, ¬ t x -> ¬(x.all fun y => s y))
     -> ∀ l : List (List a), (l.any (fun x => x.all (fun y => s y))
     -> ∀ b ∈ interl (l.filter (fun x => t x)), s b) :=
  by
  sorry

theorem forall_mem_or {b : α -> Prop}{c : α -> Prop}{e : α -> Prop}: (∀ a, (b a ∨ c a) -> e a) <-> (∀ a, b a -> e a) ∧ (∀ a, c a -> e a ) :=
  by
  sorry

theorem interl_filter_filter (d : a -> Prop)(e : List a -> Prop):
        ∀ b : a,∀ c : List (List a),
        b ∈ interl ((c.filter (fun x: List a => e x)).map (fun x => x.filter (fun y : a => (d y) )))
        -> b ∈ interl (c.filter fun x => e x) :=
  by
  sorry

theorem op2 : ∀ n : List (List (List (Bool × normalizable α pred))),
              ∀ g h : List (List (Bool × normalizable α pred)), h ∈ n -> g.all (fun x => h.any (fun y => bcompatible x y)) ->
              nToProp n -> (gToProp g <-> gToProp (g.map (fun x => x.append (interl ((h.filter (fun y => bcompatible x y)).map
              (fun y => y.filter (fun z => z ∉ x))))))) :=
  by
  intro n g hi hhi hg hn
  simp at hg
  simp
  unfold gToProp
  simp
  constructor
  intro hl
  obtain ⟨ t,ht,hht⟩ := hl
  use t
  have h_comp_exists: ∃ y ∈ hi, bcompatible t y := by {
    apply hg
    exact ht
  }
  have hhm : (hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t) ) ≠ [] := by {
    simp
    rcases h_comp_exists with ⟨y, hy_in_hi, hy_comp_t⟩
    apply List.ne_nil_of_mem
    apply List.mem_filter_of_mem
    exact hy_in_hi
    exact hy_comp_t
  }
  constructor
  exact ht
  unfold sToProp
  rw [all_and]
  constructor
  unfold sToProp at hht
  simp only [List.all_eq_true, decide_eq_true_eq]
  simp only [List.all_eq_true, decide_eq_true_eq] at hht
  exact hht
  unfold nToProp at hn
  simp only [List.all_eq_true, decide_eq_true_eq] at hn
  have hgi : gToProp hi := by {
    apply hn at hi
    apply hi at hhi
    exact hhi
  }
  unfold gToProp at hgi
  unfold sToProp at hgi
  have hfi : gToProp ((hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t))) := by{
    unfold gToProp
    have hfh : gToProp (hi.filter (fun x=> bcompatible t x)) := by {
      apply any_filter_imp (fun x => bcompatible t x) (fun x => sToProp x) at hi
      unfold gToProp
      rw [← hi]
      unfold sToProp
      exact hgi
      intro x hx
      apply compatibility at hx
      simp at hx
      simp
      apply hx
      exact hht
    }
    unfold gToProp at hfh
    unfold sToProp at hfh
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hfh
    obtain ⟨ x, hx,hhx⟩ := hfh
    simp
    use x
    constructor
    exact hx
    unfold sToProp
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hgi
    apply all_filter
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool]
    exact hhx
  }
  simp only [List.all_eq_true, decide_eq_true_eq]
  intros p ho
  apply interl_all_filter wToProp (fun y => bcompatible t y)
  intro l hlb hla
  have hlaf : sToProp l := by {
    unfold sToProp
    exact hla
  }
  apply compatibility at hlb
  apply hlb
  constructor
  exact hht
  exact hlaf
  simp only [List.all_eq_true, decide_eq_true_eq, Prod.forall
  ,  Bool.decide_and, List.any_eq_true, Bool.and_eq_true] at hgi
  simp only [List.any_eq_true, List.all_eq_true, decide_eq_true_eq, Prod.forall]
  exact hgi
  apply interl_filter_filter (fun z => !(z ∈ t)) (fun x => bcompatible t x)
  simp
  --exact ho  --for some reason this is a type mismatch
  sorry

[Julian Berman]

Great, closer, but that still doesn't work -- click on the view in playground link and you'll see it has some indentation issues I think still (in your last proof), possibly just on 2 lines but I'm not sure.

[Jared green]

try it now

[Jared green]

now?

[Kevin Buzzard]

You can just click on the little icon at the top right of the code ("View in Lean 4 playground") to check this yourself (it still doesn't work).

[Jared green]

sorry, sorry's hadnt been indented and there were some theorems i forgot to include.

[Kevin Buzzard]

The error says that you have two competing decidability instances on your type. Indeed you seem to be mixing classical and constructive logic with open Classical and [h : DecidableEq α], and also with the mixing of Bool and Prop, and this is the sort of thing which happens if you do this (not that I understand the code, maybe it's essential to use both). You can fix this by using convert instead of exact, but a better fix would be to decide whether you're working classically or constructively and sticking to it.

[Kevin Buzzard]

The error means "I figured out an actual algorithm to determine whether two terms of type Bool × normalizable α pred are equal, but also in play is the mathematicians' "algorithm" to determine this, which is "use the law of the excluded middle", and now we have a clash of algorithms, meaning that it's not exactly ho".

[Jared green]

how could i make it all classical?

[Kevin Buzzard]

Remove every occurrence of "decidable" in the file, and every time you get an error complaining that something is noncomputable, add "noncomputable" before the definition. Then exact works.

[Kevin Buzzard]

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
open Classical

set_option autoImplicit true
set_option relaxedAutoImplicit true

variable {α : Type}
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred

namespace normalizable
@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl

@[reducible]
def nStrip (n : normalizable α pred) : Bool × normalizable α pred :=
  match n with
  | Not i => (false,i)
  | i => (true,i)

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

noncomputable def bcompatible (s : List (Bool × normalizable α pred)) (t : List (Bool × normalizable α pred)) : Bool :=
  s.all (fun x => t.all (fun y =>  x.snd == y.snd -> x.fst == y.fst))

theorem compatibility :∀ a b : List (Bool × normalizable α pred),  (¬ bcompatible a b = true) -> ¬(sToProp a ∧ sToProp b) :=
  by
  sorry

theorem any_filter_imp (s t : a -> Bool): (∀ x : a, ¬ (s x) -> ¬ (t x)) -> ∀ l : List a,l.any t <-> (l.filter s).any t :=
  by
  sorry

theorem all_and : List.all ( a ++ b) c <-> List.all a c ∧ List.all b c :=
  by
  sorry

@[reducible]
noncomputable def interl (l : List (List a)) : List a :=
  match l with
  | [] => []
  | a :: [] => a
  | (a :: as) => List.inter a (interl as)

theorem interl_all (s : a -> Prop) : ∀ l : List (List a),
          l.any (fun x => x.all (fun y => s y)) -> ∀ b ∈ interl l, s b :=
  by
  sorry

theorem all_filter (s t : a -> Bool) : ∀ l : List a, l.all s -> (l.filter t).all s :=
  by
  sorry

theorem interl_all_filter (s : a -> Prop)(t : List a -> Prop) : (∀ x : List a, ¬ t x -> ¬(x.all fun y => s y))
     -> ∀ l : List (List a), (l.any (fun x => x.all (fun y => s y))
     -> ∀ b ∈ interl (l.filter (fun x => t x)), s b) :=
  by
  sorry

theorem forall_mem_or {b : α -> Prop}{c : α -> Prop}{e : α -> Prop}: (∀ a, (b a ∨ c a) -> e a) <-> (∀ a, b a -> e a) ∧ (∀ a, c a -> e a ) :=
  by
  sorry

theorem interl_filter_filter (d : a -> Prop)(e : List a -> Prop):
        ∀ b : a,∀ c : List (List a),
        b ∈ interl ((c.filter (fun x: List a => e x)).map (fun x => x.filter (fun y : a => (d y) )))
        -> b ∈ interl (c.filter fun x => e x) :=
  by
  sorry

theorem op2 : ∀ n : List (List (List (Bool × normalizable α pred))),
              ∀ g h : List (List (Bool × normalizable α pred)), h ∈ n -> g.all (fun x => h.any (fun y => bcompatible x y)) ->
              nToProp n -> (gToProp g <-> gToProp (g.map (fun x => x.append (interl ((h.filter (fun y => bcompatible x y)).map
              (fun y => y.filter (fun z => z ∉ x))))))) :=
  by
  intro n g hi hhi hg hn
  simp at hg
  simp
  unfold gToProp
  simp
  constructor
  intro hl
  obtain ⟨ t,ht,hht⟩ := hl
  use t
  have h_comp_exists: ∃ y ∈ hi, bcompatible t y := by {
    apply hg
    exact ht
  }
  have hhm : (hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t) ) ≠ [] := by {
    simp
    rcases h_comp_exists with ⟨y, hy_in_hi, hy_comp_t⟩
    apply List.ne_nil_of_mem
    apply List.mem_filter_of_mem
    exact hy_in_hi
    exact hy_comp_t
  }
  constructor
  exact ht
  unfold sToProp
  rw [all_and]
  constructor
  unfold sToProp at hht
  simp only [List.all_eq_true, decide_eq_true_eq]
  simp only [List.all_eq_true, decide_eq_true_eq] at hht
  exact hht
  unfold nToProp at hn
  simp only [List.all_eq_true, decide_eq_true_eq] at hn
  have hgi : gToProp hi := by {
    apply hn at hi
    apply hi at hhi
    exact hhi
  }
  unfold gToProp at hgi
  unfold sToProp at hgi
  have hfi : gToProp ((hi.filter (fun x => bcompatible t x)).map (fun x => x.filter (fun y => y ∉ t))) := by{
    unfold gToProp
    have hfh : gToProp (hi.filter (fun x=> bcompatible t x)) := by {
      apply any_filter_imp (fun x => bcompatible t x) (fun x => sToProp x) at hi
      unfold gToProp
      rw [← hi]
      unfold sToProp
      exact hgi
      intro x hx
      apply compatibility at hx
      simp at hx
      simp
      apply hx
      exact hht
    }
    unfold gToProp at hfh
    unfold sToProp at hfh
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hfh
    obtain ⟨ x, hx,hhx⟩ := hfh
    simp
    use x
    constructor
    exact hx
    unfold sToProp
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool, Bool.decide_and,
      List.any_eq_true, Bool.and_eq_true] at hgi
    apply all_filter
    simp only [List.all_eq_true, decide_eq_true_eq, Bool.forall_bool]
    exact hhx
  }
  simp only [List.all_eq_true, decide_eq_true_eq]
  intros p ho
  apply interl_all_filter wToProp (fun y => bcompatible t y)
  intro l hlb hla
  have hlaf : sToProp l := by {
    unfold sToProp
    exact hla
  }
  apply compatibility at hlb
  apply hlb
  constructor
  exact hht
  exact hlaf
  simp only [List.all_eq_true, decide_eq_true_eq, Prod.forall
  ,  Bool.decide_and, List.any_eq_true, Bool.and_eq_true] at hgi
  simp only [List.any_eq_true, List.all_eq_true, decide_eq_true_eq, Prod.forall]
  exact hgi
  apply interl_filter_filter (fun z => !(z ∈ t)) (fun x => bcompatible t x)
  simp
  exact ho -- now works
  sorry

[Jared green]

suppose also i need the functions bcompatible and interl to be computable?

[Kevin Buzzard]

Then you should make everything constructive and computable

[Jared green]

i went with convert, but im curious how that would look.