Proving Decidable instance with forall and exists

Stream: lean4

[Sílvio Zacomelli]

I'm trying to prove this instance of Decidable:

instance : Decidable (∃H f_n f_e, (isSubGraph H G ) ∧ (isomorphism H K33 f_n f_e ∨ isomorphism H K5 f_n f_e))

Where f_e and f_n are functions and H, G, K33 and K5 are "graphs". The functions and definitions used are in the code below:

abbrev Node := Nat

@[simp]
def unique [BEq a] (as : List a) := (as ≠ []) → ∀ a ∈ as, (as.filter (. == a)).length = 1

structure Edge where
  id: Nat
  i: Nat
  j: Nat
deriving DecidableEq, Inhabited

structure Graph where
  N : List Node
  E : List Edge
  ok : (∀ e, e ∈ E → (e.i ∈ N ∧ e.j ∈ N))
       ∧ unique N
       ∧ unique E

def K5 : Graph := K 5 (by simp;decide)
def K33 : Graph := Graph.mk [1,2,3,4,5,6] [(Edge.mk 1 1 4), (Edge.mk 2 1 5), (Edge.mk 3 1 6),(Edge.mk 4 2 4), (Edge.mk 5 2 5), (Edge.mk 6 2 6),(Edge.mk 7 3 4), (Edge.mk 8 3 5), (Edge.mk 9 3 6)] (by simp)


def isSubGraph (G H : Graph) : Prop :=
  if (∀ n, n ∈ G.N → n ∈ H.N)
   ∧ (∀ e, e ∈ G.E → ∃ d ∈ H.E, d.i = e.i ∧ d.j = e.j
      ∧ (e.i ∈ G.N ∧ e.j ∈ G.N))
  then true
  else false

def isomorphism (G H : Graph) (f_n : Node -> Node) (f_e : Edge -> Edge) : Prop :=
  if (List.map f_n G.N) = H.N ∧ (List.map f_e G.E) = H.E
  then true
  else false

For most definitions I've already implemented Decidable instances, but as the instance I'm trying to prove has a ∃H f_n f_e, I don't know how to prove it. I'm new to Lean, so proving statements with for all or exists cases always have been a problem to me. How do I prove this type of Decidable instances, that is, how do I prove the ones that have these quantifiers? Any help is appreciated (if you need to see more parts of the code just let me know and I'll post it).

[Eric Wieser]

Without commenting on the decidable instance, note that

def isomorphism (G H : Graph) (f_n : Node -> Node) (f_e : Edge -> Edge) : Prop :=
  if (List.map f_n G.N) = H.N ∧ (List.map f_e G.E) = H.E
  then true
  else false

is better written

def Isomorphism (G H : Graph) (f_n : Node -> Node) (f_e : Edge -> Edge) : Prop :=
  (List.map f_n G.N) = H.N ∧ (List.map f_e G.E) = H.E

(noting also that #naming advocates capitalization of Props)

[Kyle Miller]

Remember that creating a Decidable instance means "I am giving an algorithm to decide this", it's not something you prove. Do you have an algorithm that can find a subgraph H of G that is either isomorphic to K33 or K5 if one exists?

[Kyle Miller]

Writing the Decidable instance amounts to proving that this algorithm is correct, but you need code that computes such a graph. Or, if you have some theorem that characterizes such graphs in a different way, you could try writing an algorithm for that characterization instead.