Help with proof structure

Stream: new members

[HenrikT]

Hi everyone,
i am currently using Lean4 and created the following definitions:

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Countable
import Mathlib.Data.Finset.Basic
import Mathlib.Data.List.Basic

inductive Direction where
  | L : Direction
  | R : Direction
  | N : Direction


def directionToNum (d : Direction) : ℤ :=
  match d with
  | Direction.L => -1
  | Direction.R => 0
  | Direction.N => 1


structure Cfg where
  state : ℕ
  head : ℕ
  left : List ℕ
  right : List ℕ

structure Machine where
  Q : Finset ℕ
  Λ : Finset ℕ
  Γ : Finset ℕ
  Fₐ : Finset ℕ
  Fᵣ : Finset ℕ
  q0 : ℕ
  δ : Finset (ℕ × ℕ → ℕ × ℕ × Direction)

structure DTM  extends Machine where

  uniqueness:
    ∀ x y : (ℕ × ℕ → ℕ × ℕ × Direction),
      ∀ (a₁ a₂ : (ℕ × ℕ)), a₁ = a₂ ↔ x a₁ = y a₂


def cfgEquiv (c1 c2 : Cfg) : Prop :=
  c1.state = c2.state ∧ c1.head = c2.head ∧ c1.left = c2.left ∧ c1.right = c2.right

def updateHead (n: ℕ) (d: Direction) : ℕ :=
  match n, d with
    | 0, Direction.L => 0
    | _, Direction.R => n+1
    | _, Direction.L => n-1
    | _, Direction.N => n

def updateCfg (cfg: Cfg) (s w : ℕ) (d: Direction) : Cfg :=
  match cfg.head, d with
    | 0, Direction.L => {state := s, head := 0, left := List.nil,  right := cfg.right.modifyHead w}
    | _, Direction.L => {state := s, head := cfg.head-1, left := cfg.left.reverse.tail.reverse,  right := [w].append cfg.left}
    | _, Direction.R => {state := s, head := cfg.head+1, left := cfg.left.append [w],  right := cfg.left.tail}
    | _, Direction.N => {state := s, head := cfg.head, left := cfg.left,  right := cfg.right.modifyHead w}


def reachSucc (M : Machine) (c1 c2 : Cfg) : Prop :=
  ∃ (a γ s w : ℕ) (d : Direction), ∃ δ ∈ M.δ, δ (a, γ) = (s, w, d) ∧ cfgEquiv (updateCfg c1 s w d) c2

def isAccept (M : Machine) (cfg : Cfg)  : Prop :=
  cfg.state ∈ M.Fₐ

def isReject (M : Machine) (cfg : Cfg)  : Prop :=
  cfg.state ∈ M.Fᵣ

def isFinal (M : Machine) (cfg : Cfg)  : Prop :=
  cfg.state ∈ M.Fₐ ∨ cfg.state ∈ M.Fᵣ

def reachN (M : Machine) (n : ℕ) (c1 c2 : Cfg) : Prop :=
  if n = 0 then cfgEquiv c1 c2
  else if n = 1 then reachSucc M c1 c2
  else ∃ (c3 : Cfg), reachN M (n-1) c1 c3 ∧ reachN M (n-1) c3 c2


def finiteReach (M : Machine) (c1 c2 : Cfg) : Prop :=
  ∃ (n : ℕ), reachN M n c1 c2

def Word := List ℕ

def Word.concat (v w : Word) : Word := List.append v w
infixr:50 " + " => Word.concat

def Word.len (w: Word) : ℕ :=
  w.length

def Language := Set Word

def Language.element (w : Word) (L : Set Word) : Prop := L w
infixr:75 " ∈ " => Language.element

def Language.complement (L : Language) : Language := λ w => ¬ (w ∈ L)

def Language.notElement (w : Word) (L : Language) : Prop := L w
infixr: 75 "∉" => Language.notElement

def isDecider (M : Machine) : Prop :=
  ∀ (w : Word), ∃ (c1 c2 : Cfg), c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧
    finiteReach M c1 c2


def isEnumerator (M : Machine) (L : Language) : Prop :=
  ∀ (w : Word), w ∈ L → ∃ (c1 c2 : Cfg), c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧
    isAccept M c2 → finiteReach M c1 c2


def isSemiDecider (M : Machine) : Prop :=
  ∀ (w : Word), ∃ (c1 c2 : Cfg), c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧
    isAccept M c2 → finiteReach M c1 c2

def isCoSemiDecider (M : Machine) : Prop :=
  ∀ (w : Word), ∃ (c1 c2 : Cfg), c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧
    isReject M c2 → finiteReach M c1 c2


def semi_decidable (L : Language) : Prop :=
  ∃ (M : Machine), ∀ (w : Word), ∃ (c1 c2 : Cfg),
    (w ∈ L → c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧ finiteReach M c1 c2 ∧ isAccept M c2)

def co_semi_decidable (L : Language) : Prop :=
  ∃ (M : Machine), ∀ (w : Word), ∃ (c1 c2 : Cfg),
    (w ∉ L → c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧ finiteReach M c1 c2 ∧ isReject M c2)

def decidable (L : Language) : Prop :=
  ∃ (M : Machine), ∀ (w : Word), ∃ (c1 c2 : Cfg),
    ((w ∈ L → c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧ finiteReach M c1 c2 ∧ isAccept M c2) ∧
    (w ∉ L → c1 = {state := 0, head := 0, left := List.nil,  right := w} ∧ finiteReach M c1 c2 ∧ isReject M c2))

I then defined the following Theorem

theorem CoSemiAndSemiEqDescidable (L : Language) : decidable L ↔ (semi_decidable L ∧ co_semi_decidable L) :=
    sorry

Because i am pretty new to this i do not know how to proof this using Lean4.
I started by creating two goal (one for each direction) using apply Iff.intro then unfolded my definitions but then got more or less stuck.
Any idea on how to proceed ?

Thanks in advance :)

[Martin Dvořák]

Please provide imports.
#mwe

[HenrikT]

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.List
import Mathlib.Data.Finset.Basic
import Mathlib.Data.List.Basic


def Word := List ℕ
def Language := Set Word


structure Cfg where
  state : ℕ
  head : ℕ
  left : List ℕ
  right : List ℕ

structure Machine where
  Q : Finset ℕ
  Λ : Finset ℕ
  Γ : Finset ℕ
  Fₐ : Finset ℕ
  Fᵣ : Finset ℕ
  q0 : ℕ
  δ : Finset (ℕ × ℕ → ℕ × ℕ × Direction)

[Martin Dvořák]

Where is finiteReach defined?

[HenrikT]

I defined it in the same file. I was not sure how much code i should post.

the definitions look as follows:

inductive Direction where
  | L : Direction
  | R : Direction
  | N : Direction

def cfgEquiv (c1 c2 : Cfg) : Prop :=
  c1.state = c2.state ∧ c1.head = c2.head ∧ c1.left = c2.left ∧ c1.right = c2.right

def reachSucc (M : Machine) (c1 c2 : Cfg) : Prop :=
  ∃ (a γ s w : ℕ) (d : Direction), ∃ δ ∈ M.δ, δ (a, γ) = (s, w, d) ∧ cfgEquiv (updateCfg c1 s w d) c2

def isAccept (M : Machine) (cfg : Cfg)  : Prop :=
  cfg.state ∈ M.Fₐ

def isReject (M : Machine) (cfg : Cfg)  : Prop :=
  cfg.state ∈ M.Fᵣ

def isFinal (M : Machine) (cfg : Cfg)  : Prop :=
  cfg.state ∈ M.Fₐ ∨ cfg.state ∈ M.Fᵣ

def reachN (M : Machine) (n : ℕ) (c1 c2 : Cfg) : Prop :=
  if n = 0 then cfgEquiv c1 c2
  else if n = 1 then reachSucc M c1 c2
  else ∃ (c3 : Cfg), reachN M (n-1) c1 c3 ∧ reachN M (n-1) c3 c2


def finiteReach (M : Machine) (c1 c2 : Cfg) : Prop :=
  ∃ (n : ℕ), reachN M n c1 c2

[Martin Dvořák]

You should post as much code as we need to replicate your issue.
#mwe

[Martin Dvořák]

Where is updateCfg defined?

[HenrikT]

def updateCfg (cfg: Cfg) (s w : ℕ) (d: Direction) : Cfg :=
  match cfg.head, d with
    | 0, Direction.L => {state := s, head := 0, left := List.nil,  right := cfg.right.modifyHead w}
    | _, Direction.L => {state := s, head := cfg.head-1, left := cfg.left.reverse.tail.reverse,  right := [w].append cfg.left}
    | _, Direction.R => {state := s, head := cfg.head+1, left := cfg.left.append [w],  right := cfg.left.tail}
    | _, Direction.N => {state := s, head := cfg.head, left := cfg.left,  right := cfg.right.modifyHead w}

[Martin Dvořák]

#mwe
"so others can simply just cut and paste what you post, and see the same issue that you are seeing"

[HenrikT]

for the language i also defined the following

def Language.element (w : Word) (L : Set Word) : Prop := L w
infixr:75 " ∈ " => Language.element

-- failed to synth. instance membership Word Language ?
def Language.complement (L : Language) : Language := λ w => ¬ (w ∈ L)

def Language.notElement (w : Word) (L : Language) : Prop := L w
infixr: 75 "∉" => Language.notElement

[Martin Dvořák]

Please click on the blue thing #mwe and follow the instructions.

[HenrikT]

ok i keep that in mind for next time, sorry for the confusion :)

[Martin Dvořák]

For the next time and for this time as well. Please. Give me a code that I can compile.

In case you don't want to copypaste too many lines of code, you can provide a link to a repository instead. However, I am fine with copypasting a long block of code IF IT WORKS.

[Notification Bot]

HenrikT has marked this topic as resolved.

[Notification Bot]

HenrikT has marked this topic as unresolved.

[Martin Dvořák]

Ah. You updated the original post! I'll have a look at it.

[HenrikT]

yes thanks for your patience. The problem is, that i used two files instead of one hence its a bit difficulty with just copy past. I hope it works now though :)

[Martin Dvořák]

This is how you can prove one of the "trivial" parts:

theorem CoSemiAndSemiEqDescidable (L : Language) : decidable L ↔ (semi_decidable L ∧ co_semi_decidable L) := by
  constructor
  · intro ⟨M, hM⟩
    constructor
    · unfold semi_decidable
      use M
      intro w
      specialize hM w
      rcases hM with ⟨c₁, c₂, h_yesin, h_notin⟩
      use c₁
      use c₂
      exact h_yesin
    · sorry
  · sorry

I suggest you play with it yourself and let us know when you encounter a major obstacle.

[HenrikT]

ok thanks a lot ill have a look at it

[Martin Dvořák]

Discharging the first sorry is straightforward. However, for the second implication, you will have to construct a new machine, which will be much more difficult.

[Martin Dvořák]

Note that in the part I provided "nothing" happens — I just took the assumption and threw away one part.

[Martin Dvořák]

This is not really educational but possibly useful:

theorem DecidableIff (L : Language) : decidable L ↔ (semi_decidable L ∧ co_semi_decidable L) := by
  constructor
  · intro ⟨M, hM⟩
    constructor <;> use M <;> intro w <;> rcases hM w with ⟨c₁, c₂, w_yesin, w_notin⟩
    · exact ⟨c₁, c₂, w_yesin⟩
    · exact ⟨c₁, c₂, w_notin⟩
  · sorry

[HenrikT]

thanks having an example to look at realy helps with understanding how Lean works

[Martin Dvořák]

If I can give a general advice, write more definitions and avoid stuff like:

{state := s, head := 0, left := List.nil,  right := cfg.right.modifyHead w}

[HenrikT]

ok ill try to keep that in mind

[Martin Dvořák]

If the issue is understanding Lean, I suggest you start with easier material. Like the Natural Number Game:
https://adam.math.hhu.de/#/g/hhu-adam/NNG4

[HenrikT]

i did not know there was a LEAN4 version i only found the Lean3 version

[HenrikT]

ill have a look at it

[Martin Dvořák]

NNG4 is pretty new!

[HenrikT]

Ok guess i play abit arond in NNG4. If anything else pops up regarding the proof ill let you know

[Martin Dvořák]

HenrikT said:

I defined it in the same file.
(...)

FYI, I didn't check whether your definitions make sense as a Turing machine. I was just treating it as a black box.

If you really want to play with Turing machines, I suggest that (before you do any theorems) you define an example and check whether you can walk through its computation in the way you intended.

[HenrikT]

ok :+1: