Writing theorem for proposition.

Stream: general

[Tamas Hadhazy]

How would I write a theorem and prove this proposition?

structure NodeRef where
    nid: Nat
deriving Inhabited, Repr, BEq, DecidableEq

structure NodeTest where
  ref : NodeRef
  inputs : Array NodeRef := #[]
  outputs : Array NodeRef := #[]

def inputsOutputsConsistent (nodes : Array NodeTest) : Prop :=
  ∀ (a x : NodeTest),
    a ∈ nodes →
    x ∈ nodes →
    x.ref ∈ a.inputs →
    a.ref ∈ x.outputs

def test1plus2 : NodeTest :=
  { ref := {nid := 0}, inputs := #[{nid := 1}, {nid := 2}], outputs := #[] }

def test1 : NodeTest :=
  { ref := {nid := 1}, inputs := #[], outputs := #[{nid := 0}] }

def test2 : NodeTest :=
  { ref := {nid := 2}, inputs := #[], outputs := #[{nid := 0}] }

-- Put all nodes in an array
def testGraph : Array NodeTest := #[test1plus2, test1, test2]

[Aaron Liu]

What theorem do you want to write

[Aaron Liu]

Also, you don't need to mark your code as haskell, the default on this zulip is lean4

[Tamas Hadhazy]

I want to prove that if a node x has an input called b then in node b's outputs we have to find node x and vice versa.
see

    x.ref ∈ a.inputs →
    a.ref ∈ x.outputs

[Aaron Liu]

you want to prove this?

example : inputsOutputsConsistent testGraph := by
  sorry

[Aaron Liu]

here's my proof btw

proof

example : inputsOutputsConsistent testGraph := by
  unfold inputsOutputsConsistent testGraph test1plus2 test1 test2
  simp only [List.mem_toArray, List.mem_cons, List.mem_nil_iff, or_imp, forall_and,
    forall_eq_apply_imp_iff, forall_eq]
  simp

[Tamas Hadhazy]

Can you, by any chance, give me a description of what these are doing?

[Tamas Hadhazy]

It works fine btw.

[Aaron Liu]

unfold will unfold the declarations

[Aaron Liu]

simp is the simplifier, it uses the theorems tagged @[simp] to simplify stuff into something provably equal

[Aaron Liu]

simp only means don't use the theorems tagged @[simp], actually only use the theorems I give it to simplify stuff

[Tamas Hadhazy]

You can only use unfold on reducible definitions, right?

Here why do you need testGraph test1plus2 test1 test2 for the unfold inputsOutputsConsistent

[Aaron Liu]

it can unfold most definitions

[Aaron Liu]

unfold foo1 foo2 is mostly the same as unfold foo1; unfold foo2

[Tamas Hadhazy]

so here you are unfolding
inputsOutputsConsistent, testGraph, test1plus2, test1, test2?

[Tamas Hadhazy]

So all of these are lemmas right?

  simp only [List.mem_toArray, List.mem_cons, List.mem_nil_iff, or_imp, forall_and,
    forall_eq_apply_imp_iff, forall_eq]

[Aaron Liu]

those lemmas are lemmas I am telling simp to use to rewrite the goal

[Tamas Hadhazy]

So now I want to prove

def nodeControl (nodes : Array NodeTest) : Prop :=
  ∀ n ∈ nodes,
    (n.inputs.isEmpty ∧ isCfg n) ∨
    (¬ n.inputs.isEmpty ∧
      let firstRef := n.inputs[0]!
      ∃ ctrl ∈ nodes, ctrl.ref = firstRef ∧ isCfg ctrl)

and I did

example : nodeControl testGraph := by
  unfold nodeControl testGraph starttest1plus2 test1plus2 test1 test2
  simp only [List.mem_toArray, List.mem_cons, List.mem_nil_iff, or_imp, forall_and,
    forall_eq_apply_imp_iff, forall_eq]
  simp

but it still gives me unsolved goals

[Aaron Liu]

well you can't expect the same proof to work for every theorem

[Tamas Hadhazy]

I guess the "logical disjunction" and "logical conjunction" make it different so probably will need other tools

[Tamas Hadhazy]

@Aaron Liu do you have any idea about how I might be able to prove it?

[Aaron Liu]

no I don't

[Aaron Liu]

since I have no idea what isCfg does

[Tamas Hadhazy]

Just checking if it is a CFG node or not

inductive NodeDataTest where
  | constantl (value: Int)
  | nullData
  | returnData
  | startData
deriving Inhabited, Repr, BEq, DecidableEq

structure NodeTest where
  ref : NodeRef
  data: NodeDataTest
  inputs : Array NodeRef := #[]
  outputs : Array NodeRef := #[]



def isCfg(node: NodeTest) :=
 match node.data with
  | NodeDataTest.startData => true
  | NodeDataTest.returnData => true
  | _ => false

[Aaron Liu]

this all looks like very decidable stuff

[Aaron Liu]

why don't you try writing a Decidable instance

[Tamas Hadhazy]

So just use the decide tactic?