Zulip Chat Archive

Stream: Is there code for X?

Topic: Matrix on edge set for graphs


view this post on Zulip Gabriel Moise (Mar 05 2021 at 11:44):

Hello!
I am trying to define the incidence matrix of a graph, but currently fail to do so using the edge set of the graph. Is there any code for that i.e. where the edge set of the graph is used as a fintype for the matrix?

variables (G : simple_graph V) [decidable_rel G.adj] [decidable_eq V]  [preorder V]

-- Some attempts, unsuccessful
--variables (E : finset (sym2 V))
--def E := G.edge_set.to_finset

def incidence_matrix : matrix V E 
| i e := if e  (G.incidence_finset i) then 1 else 0

What I am currently struggling is creating E such that E is a fintype, and also E is the edge set of V so that I can define the incidence matrix of G properly.

view this post on Zulip Johan Commelin (Mar 05 2021 at 11:50):

@Alena Gusakov @Kyle Miller will probably know. But I think the adjacency matrix is already defined somewhere.

view this post on Zulip Gabriel Moise (Mar 05 2021 at 11:50):

Yes, but the adjancency matrix is defined on the set of vertices V, what I am looking for is a matrix defined on the edge set, if that makes sense.

view this post on Zulip Johan Commelin (Mar 05 2021 at 11:51):

Ooh, sorry. I don't know much about graphs

view this post on Zulip Johan Commelin (Mar 05 2021 at 11:52):

Can you use {e // e \in G.edge_set}?

view this post on Zulip Johan Commelin (Mar 05 2021 at 11:52):

That should give you a type, and hopefully Lean figures out automatically that it is finite if V is finite.

view this post on Zulip Gabriel Moise (Mar 05 2021 at 11:57):

So, although we have from the simple_graph file that:

def edge_set : set (sym2 V) := sym2.from_rel G.sym

When I define my set E as:

def E : set (sym2 V) := {e // e  G.edge_set} -- btw what does // mean? is it like the mathematical notation {x | x \in \N, x < 3} or something like that?

I get the error

type mismatch, term
  {e // e  G.edge_set}
has type
  Type u : Type (max 1 (u+1))
but is expected to have type
  set (sym2 V) : Type u

view this post on Zulip Johan Commelin (Mar 05 2021 at 12:07):

matrix expects a type n with an instance fintype n. you are trying to feed it a set.

view this post on Zulip Johan Commelin (Mar 05 2021 at 12:08):

{x // condition on x} creates a Type* which you can then use for matrix.

view this post on Zulip Johan Commelin (Mar 05 2021 at 12:08):

But it still needs the fintype instance.

view this post on Zulip Gabriel Moise (Mar 05 2021 at 12:14):

Oh, now I see. Ok, so after the fixes, the thing that is left is this:

def E := {e // e  G.edge_finset}
def inc_matrix : matrix V E 

which gives the error:

type mismatch at application
  matrix V E
term
  E
has type
    Type ? : Type (max ? 1 (?+1))
but is expected to have type
  Type ? : Type (?+1)

Can you please explain what the error means? I often come across error messages like this, but can't see what they precisely mean.

view this post on Zulip Eric Wieser (Mar 05 2021 at 12:17):

Lean definitely can't find fintype E there, as you hid it behind a def

view this post on Zulip Alena Gusakov (Mar 05 2021 at 14:53):

I wonder if you might be able to just have [fintype G.edge_set] for this?

view this post on Zulip Alena Gusakov (Mar 05 2021 at 14:53):

I know fintype/finset stuff is really annoying

view this post on Zulip Gabriel Moise (Mar 05 2021 at 15:07):

Can't seem to make it work with that idea, this is how I managed to do it for now, I know it's ugly, but I will improve it when I myself improve at Lean probably :smile:

def E : Type u := {e // e  G.edge_set}

instance edges_fintype' [decidable_eq V] [fintype V] [decidable_rel G.adj] :
  fintype G.E := subtype.fintype _

instance has_mem : has_mem V G.E := { mem := λ v e, v  e.val }

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.E  -- maybe use ℕ instead of ℤ?
| i e := if i  e then 1 else 0

Oh, and I don't seem to find any library containing directed graphs, since I might need them to define the directed incidence matrix. Is there some work in progress towards that? (this is just for learning purposes towards my project, don't want to copy anybody :smile: )

view this post on Zulip Kyle Miller (Mar 05 2021 at 17:24):

I'd suggest not defining E and instead use Lean's auto-coercion feature:

import combinatorics.simple_graph.basic
import linear_algebra.matrix

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  -- maybe use ℕ instead of ℤ?
| i e := if i  e.val then 1 else 0

(By the way, there's also e.val ∈ G.incidence_set i for indicating that an edge and a vertex are incident. It means exactly the same thing as i ∈ e.val but potentially has more useful lemmas about it.)

view this post on Zulip Kyle Miller (Mar 05 2021 at 17:31):

Gabriel Moise said:

Oh, and I don't seem to find any library containing directed graphs, since I might need them to define the directed incidence matrix. Is there some work in progress towards that? (this is just for learning purposes towards my project, don't want to copy anybody :smile: )

There's nothing about directed graphs yet. For directed incidence matrices, I've thought it would be nice if there were a type of directed simple graphs, a function to simple_graph that forgets orientations, and a function to prove/calculate things about simple graphs by giving a proof/calculation for directed graphs and a proof that changing the orientation of an edge doesn't change the result. This could be how you'd use directed incidence matrices for a simple graph. (One example: calculate the graph Laplacian from IITII^T for II a directed incidence matrix of a directed version of a given simple graph.)

view this post on Zulip Peter Nelson (Mar 06 2021 at 02:23):

By the time you are talking about an incidence matrix, it will get increasingly cumbersome to think of edges as certain pairs of vertices. Instead, you can model a graph as an incidence structure on a vertex type V and an edge type E together with some some incidence information (such as inc : V \to E \to \nat or head : E \to V, tail : E \to V), the flavour of which could capture simple graphs, multigraphs, digraphs, hypergraphs, etc etc. Defining an incidence matrix is easy if you set things up this way. For directed graphs, I personally like inc : V \to E \to int which takes values 1 and -1.

In some areas of graph theory, such as when you're thinking about induced subgraphs and complements, an edge really 'is' a pair of vertices. However, in other cases, you really want to think of edges as their own entities that are not syntactically bound to vertices. If you want an incidence matrix, this strongly suggests to me that you're in the latter situation.

view this post on Zulip Gabriel Moise (Mar 07 2021 at 13:35):

Kyle Miller said:

I'd suggest not defining E and instead use Lean's auto-coercion feature:

import combinatorics.simple_graph.basic
import linear_algebra.matrix

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  -- maybe use ℕ instead of ℤ?
| i e := if i  e.val then 1 else 0

(By the way, there's also e.val ∈ G.incidence_set i for indicating that an edge and a vertex are incident. It means exactly the same thing as i ∈ e.val but potentially has more useful lemmas about it.)

Following this approach, I get into some trouble with type coercions, for example, here I want to prove something quite simple :

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i =  (e : G.edge_set), G.inc_matrix i e :=
begin
  unfold inc_matrix,
  simp [finset.sum_ite],
  rw  card_incidence_set_eq_degree,
  sorry
end

which is very similar to what is already done in the simple_graph module, however I stumble upon the following thing:

fintype.card (G.incidence_set i) = (filter (λ (x : (G.edge_set)), x  G.incidence_set i) univ).card

which is what is left to be proven, but I can't seem to get it done, as I am not very experienced with coercions. My fear is that I will encounter this a lot and it would make code look messy.

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 13:39):

Can you give a #mwe?

view this post on Zulip Gabriel Moise (Mar 07 2021 at 13:39):

Peter Nelson said:

By the time you are talking about an incidence matrix, it will get increasingly cumbersome to think of edges as certain pairs of vertices. Instead, you can model a graph as an incidence structure on a vertex type V and an edge type E together with some some incidence information (such as inc : V \to E \to \nat or head : E \to V, tail : E \to V), the flavour of which could capture simple graphs, multigraphs, digraphs, hypergraphs, etc etc. Defining an incidence matrix is easy if you set things up this way. For directed graphs, I personally like inc : V \to E \to int which takes values 1 and -1.

In some areas of graph theory, such as when you're thinking about induced subgraphs and complements, an edge really 'is' a pair of vertices. However, in other cases, you really want to think of edges as their own entities that are not syntactically bound to vertices. If you want an incidence matrix, this strongly suggests to me that you're in the latter situation.

With this approach, I see that I can do something like

structure graph (V : Type u) (E : Type v) :=
(incidence : V  E  )

However, if I want to define a simple_graph as a special case for the more general graph (I am not sure it is necessary for me to do that though, just felt it might be needed), I thought this would work:

def simple_graph (V : Type u) [decidable_eq V] : graph V (sym2 V) :=
{incidence := λ i e, if (i  e)  (¬ sym2.is_diag e) then 1 else 0}

However, this looks much more "unfriendly" than the usual structure of a simple_graph from the library and it doesn't look like I can do much with it right away.

view this post on Zulip Gabriel Moise (Mar 07 2021 at 13:50):

Yakov Pechersky said:

Can you give a #mwe?

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators matrix
open finset matrix simple_graph

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set 
| i e := if e.val  G.incidence_set i then 1 else 0

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i =  (e : G.edge_set), G.inc_matrix i e :=
begin
  unfold inc_matrix,
  simp [finset.sum_ite],
  rw  card_incidence_set_eq_degree,
  sorry,
end

end simple_graph

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:22):

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  -- maybe use ℕ instead of ℤ?
| i e := if i  e.val then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite (i  e.val) 1 0 := rfl

lemma mem_edge_set_of_incidence {G : simple_graph V} {e : sym2 V} {v : V}
  (h : e  G.incidence_set v) : e  G.edge_set :=
set.mem_of_mem_inter_left h

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i =  (e : G.edge_set), G.inc_matrix i e :=
begin
  rw inc_matrix_def,
  simp only [finset.sum_ite, add_zero, mul_one, nat.cast_id, finset.sum_const, nsmul_eq_mul, finset.sum_const_zero,
  subtype.val_eq_coe],
  rw  card_incidence_set_eq_degree,
  have : G.incidence_set i = G.incidence_finset i,
    { ext, simp },
  simp_rw this,
  have := fintype.card_coe (G.incidence_finset i),
  convert this using 1,
  { congr },
  { refine finset.card_congr _ _ _ _,
    { intros e he,
      exact e },
    { intros e he,
      simpa [incidence_finset, incidence_set] using he },
    { intros e1 e2 he1 he2 h,
      ext,
      simp only at h,
      simp [h] },
    { intros e he,
      rw mem_incidence_finset at he,
      use [e, mem_edge_set_of_incidence he],
      refine _, _⟩,
      { simpa [incidence_set] using he.right },
      { simp } } }
end

end simple_graph

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:23):

That's solving your current problem. I had to provide two tiny pieces of API.

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:23):

In general, I think there are likely better ways to phrase it such that you don't have to juggle between fintype, finsets, and various coercions.

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:35):

Here's another version, pick your poison.

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  -- maybe use ℕ instead of ℤ?
| i e := if (e : sym2 V)  G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V)  G.incidence_set i) 1 0 := rfl

lemma mem_edge_set_of_incidence {G : simple_graph V} {e : sym2 V} {v : V}
  (h : e  G.incidence_set v) : e  G.edge_set :=
set.mem_of_mem_inter_left h

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i =  (e : G.edge_set), G.inc_matrix i e :=
begin
  rw inc_matrix_def,
  rw  card_incidence_set_eq_degree,
  simp only [finset.sum_boole, nat.cast_id],
  refine finset.card_congr _ _ _ _,
  { rintros e, he he',
    exact e, mem_edge_set_of_incidence he },
  { rintros e, he he',
    simpa using he },
  { rintros e1, he1 e2, he2 he1' he2' h,
    ext,
    simp only [subtype.mk_eq_mk] at h,
    simp [h], },
  { rintros e, he he',
    use [e],
    { simpa using he' },
    { simp } }
end

end simple_graph

view this post on Zulip Gabriel Moise (Mar 07 2021 at 14:39):

Woah, thank you very much! I will try to use a different approach, cause this is actually a lot of work for such a result, so I guess I need a change.

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:43):

If you check the simps, you'll see absolutely no content about graphs

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:44):

So that just means some finset/fintype API is missing

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:44):

One minute

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:47):

Like so:

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

lemma fintype.card_coe_filter {α : Sort*} {s t : set α} [fintype s] [fintype t]
  [decidable_pred (λ (x : t), (x : α)  s)] (h : s  t) :
  fintype.card s = finset.card (finset.filter (λ (x : t), (x : α)  s) finset.univ) :=
begin
  refine finset.card_congr _ _ _ _,
  { rintros e, he he',
    exact e, h he },
  { rintros e, he he',
    simpa only [true_and, finset.mem_univ, finset.mem_filter] using he},
  { rintros e1, he1 e2, he2 he1' he2' hr,
    ext,
    simp only [subtype.mk_eq_mk] at hr,
    simp only [hr] },
  { rintros e, he he',
    use [e],
    { simpa only [true_and, finset.mem_univ, finset.mem_filter] using he'},
    { simp only [finset.mem_univ, exists_prop_of_true] } }
end

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  -- maybe use ℕ instead of ℤ?
| i e := if (e : sym2 V)  G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V)  G.incidence_set i) 1 0 := rfl

lemma mem_edge_set_of_incidence {G : simple_graph V} {e : sym2 V} {v : V}
  (h : e  G.incidence_set v) : e  G.edge_set :=
set.mem_of_mem_inter_left h

lemma incidence_subset_edge_set (G : simple_graph V) (v : V) : G.incidence_set v  G.edge_set :=
λ _, set.mem_of_mem_inter_left

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i =  (e : G.edge_set), G.inc_matrix i e :=
begin
  rw [inc_matrix_def, card_incidence_set_eq_degree],
  simpa using fintype.card_coe_filter (G.incidence_subset_edge_set i)
end

end simple_graph

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 14:48):

Now you can see that your statement is very simple, and is just the result of the simple implication that any incidence_set is definitionally a subset of the edge_set.

view this post on Zulip Gabriel Moise (Mar 07 2021 at 14:58):

Oh, I see what you mean. So, I should either get used to working with finsets and fintypes to continue with this model, or choose a different model.

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 15:00):

I see this as just part of the formalization. You have to identify which pieces of what you're working on are the "mathematical content" and which is the "fomalization plumbing". Separating out the two is the skill I've had to gain to be able to do the formalizations I am interested in

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 15:03):

In addition, graphs might be some of the more frustrating things in formalization because of the constant jumps between objects, subobjects, choice, finite vs infinite, many different "induction principles"

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 15:03):

And working with concrete objects too.

view this post on Zulip Gabriel Moise (Mar 07 2021 at 15:06):

Well, I guess I will become good at them with experience and I will see what tools I need to formalize what I want. I will see what I can do to progress with what you proved for me! Thank you again! :smile:

view this post on Zulip Kyle Miller (Mar 08 2021 at 05:55):

By the way, incidence_subset_edge_set already exists as simple_graph.incidence_set_subset.

import combinatorics.simple_graph.basic
import linear_algebra.matrix

lemma fintype.card_coe_filter {α : Sort*} {s t : set α} [fintype s] [fintype t]
  [decidable_pred (λ (x : t), (x : α)  s)] (h : s  t) :
  fintype.card s = (finset.filter (λ (x : t), (x : α)  s) finset.univ).card :=
begin
  refine finset.card_congr _ _ _ _,
  { exact λ e, he _, e, h he },
  { rintros e, he _,
    simpa only [true_and, finset.mem_univ, finset.mem_filter] using he },
  { rintros e1, he1 e2, he2 _ _ hr,
    simpa only [subtype.mk_eq_mk] using hr },
  { rintros e, he he',
    simpa only [true_and, exists_prop, finset.mem_univ, set_coe.exists,
      subtype.mk_eq_mk, exists_eq_right, finset.mem_filter] using he' }
end

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  :=
λ i e, if (e : sym2 V)  G.incidence_set i then 1 else 0

lemma degree_equals_sum_of_incidence_row {i : V} :
  G.degree i =  (e : G.edge_set), G.inc_matrix i e :=
by rw [inc_matrix, finset.sum_boole, nat.cast_id,
       fintype.card_coe_filter (G.incidence_set_subset i), card_incidence_set_eq_degree]

end simple_graph

view this post on Zulip Gabriel Moise (Mar 09 2021 at 12:03):

Can I get some help with this, I encounter this situation very often, when I have to prove stuff about the sum of elements from a type, but I struggle with splitting the sum into two parts based on some property: in the following case, I know that the sum can be split into the sum where x is not the edge between i and j (in which case the sum is 0) and the sum (consisting of one element) when x is the edge (therefore the sum will be 1) and altogether the sum will equal 1 as I need. Can you give me a direction regarding this kind of problems?

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  -- maybe use ℕ instead of ℤ?
| i e := if (e : sym2 V)  G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V)  G.incidence_set i) 1 0 := rfl

lemma adj_sum_of_prod_inc_one {i j : V} :
G.adj i j   (x : (G.edge_set)), G.inc_matrix i x * G.inc_matrix j x = 1 :=
begin
  intro hyp,
  -- If x is the edge between i and j, then the product is 1, else it is 0, and since there is only
  -- one edge between i and j, the sum will be 1
  sorry
end

end simple_graph

view this post on Zulip Johan Commelin (Mar 09 2021 at 12:06):

There is finset.sum_filter that might be helpful for that

view this post on Zulip Eric Wieser (Mar 09 2021 at 12:11):

Your statement is probably easier to prove as:

def inc_matrix : matrix V (sym2 V)  := -- maybe use ℕ instead of ℤ?
λ i e, if e  G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V)  G.incidence_set i) 1 0 := rfl

lemma adj_sum_of_prod_inc_one {i j : V} :
G.adj i j   x in G.edge_finset, G.inc_matrix i x * G.inc_matrix j x = 1 :=

The subtype and coercion stuff is a distraction

view this post on Zulip Eric Wieser (Mar 09 2021 at 12:17):

This is a good start:

lemma adj_sum_of_prod_inc_one {i j : V} :
G.adj i j   x in G.edge_finset, G.inc_matrix i x * G.inc_matrix j x = 1 :=
begin
  intro hyp,
  have : (i, j)  G.edge_finset := (G.mem_edge_finset _).mpr hyp,
  rw finset.insert_erase this,
  rw finset.sum_insert (finset.not_mem_erase _ _),
  convert add_zero 1,
  { sorry, },
  { apply finset.sum_eq_zero,
    intros x hx,
    rw finset.mem_erase at hx,
    sorry}
end

view this post on Zulip Gabriel Moise (Mar 09 2021 at 12:56):

Wouldn't it be a mistake to define the incidence matrix on the whole sym2 V type? Like it's definition is on the edge set of the graph from what I know.

view this post on Zulip Yakov Pechersky (Mar 09 2021 at 13:28):

When defined over the whole sym2 V type, you'll just have all zero columns

view this post on Zulip Gabriel Moise (Mar 09 2021 at 13:42):

Yes, I see that, but I thought it would have been better to follow the mathematical definition of the incidence matrix, but I guess that this solves me a lot of coercion problems since I don't have the G.edge_set type anymore.

view this post on Zulip Eric Wieser (Mar 09 2021 at 13:48):

You're always free to have separate inc_matrix' and inc_matrix definitions, where one is the mathetmatically "clean" one, while the other is the one that is easy to prove things about

view this post on Zulip Eric Wieser (Mar 09 2021 at 13:49):

Then all you need is a lemma saying how they relate to each other

view this post on Zulip Kyle Miller (Mar 10 2021 at 07:12):

@Gabriel Moise There's a missing graph theory lemma that makes this easier. After that, the main (non-math) complexity is to get things into the right form for finset.filter_eq.

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set  :=
λ i e, if (e : sym2 V)  G.incidence_set i then 1 else 0

lemma inc_matrix_apply (i : V) (e : G.edge_set) :
  G.inc_matrix i e = if (e : sym2 V)  G.incidence_set i then 1 else 0 := rfl

lemma mem_incidence_sets_iff_eq_of_adj {i j : V} (h : G.adj i j) (e : sym2 V) :
  e  G.incidence_set i  e  G.incidence_set j  e = (i, j) :=
begin
  refine quotient.rec_on_subsingleton e (λ p, _),
  rcases p with v, w⟩,
  rw sym2.eq_iff,
  simp only [incidence_set],
  tidy,
end

lemma adj_sum_of_prod_inc_one {i j : V} (h : G.adj i j) :
   (e : G.edge_set), G.inc_matrix i e * G.inc_matrix j e = 1 :=
begin
  simp only [inc_matrix_apply, ite_and, G.mem_incidence_sets_iff_eq_of_adj h,
    finset.sum_boole, nat.cast_id, boole_mul],
  have key := congr_arg finset.card (finset.filter_eq finset.univ (⟨(i, j), h : G.edge_set)),
  simp only [finset.mem_univ, if_true, finset.card_singleton] at key,
  convert key,
  ext x,
  cases x,
  simp only [subtype.coe_mk],
  exact eq_comm,
end

end simple_graph

view this post on Zulip Gabriel Moise (Mar 12 2021 at 19:12):

There is also one thing that always appears in my proofs and I always improvise with lemma's that I create specifically for the current thing I am solving, but I was wondering if there is a simple proof for this:

import linear_algebra.matrix

open_locale big_operators

universe u
variables {V : Type u} [fintype V]

lemma sum_simplification {x : V} (f g : V -> ) (h : V   -> ) (P : V  Prop)
[decidable_pred P] :
 (x : V), h x (ite (P x) (f x) (g x)) =
 (x : V), ite (P x) (h x (f x)) (h x (g x)) :=
begin
  sorry,
end

It is close to the lemma "sum_apply_ite", however there the function h that is applied is independent of x. I apologize for the narrowing to \Z, but this will perfectly do for my work. I don't need a full solution, some hints are more than welcomed as well :smile:

view this post on Zulip Eric Wieser (Mar 12 2021 at 19:35):

I think you want docs#apply_ite?

view this post on Zulip Gabriel Moise (Mar 12 2021 at 19:45):

Oh I forgot about working on the internal elements, thank you so much! :smile:


Last updated: May 19 2021 at 00:40 UTC