Matroids - How to define?

Stream: maths

[Peter Nelson]

I'm interested in formalizing the combinatorial theory of matroids. After working on this / learning Lean for the last week or so, I am running into some basic issues with definitions that I don't know the solution to. This (somewhat long) post is an appeal for help. I will try to give the minimum amount of information to indicate what my problems are.

There are many equivalent definitions of a matroid, but the one I am interested in is the following: a matroid is a pair (E,r), where E is a finite 'ground' set, and r is a function assigning a nonegative integer 'rank' to each subset X of E, so that three axioms are satisfied:

R1 : ∀ X ⊆ E, r(X) ≤ |X|
R2 : ∀ X ⊆ Y ⊆ E, r(X) ≤ r (Y)
R3 : ∀ X ⊆ Y ⊆ E, r (X ∪ Y) + r (X ∩ Y) ≤ r(X) + r(Y) .

The exact nature of the second and third axioms is not particularly important. It is somewhat important that cardinality appears in the first one though; this is one of the many reasons that matroids need to be finite, which is seemingly the source of a few of the problem I'm encountering.

To give an idea of the kind of statements about matroids I would like to prove, I ask that you bear with me while I give three other definitions and one lemma statement.

Given a set A ⊆ E, one can 'remove' A from M in two different ways to obtain matroids with ground set E \ A. the 'deletion' M \ A is just the matroid obtained from M by restricting the rank function to the domain E \ A. The 'contraction' M/A is the matroid on ground set E \ A with rank function r' defined by r'(X) = r(X ∪ A) - r(A). The deletion is trivially a matroid, and it is an easy exercise to show that the contraction is a matroid. Finally, the 'dual' of a matroid M = (E,r) is the matroid M* = (E,r') with rank function defined by r'(X) = |X| - r(E) + r(E \ X). It is also easy to show that M* is a matroid, and to prove the following:

Lemma: For all A ⊆ E we have (M / A)* = M* \ D.

That is, contraction and deletion are dual operations. These statements all seem simple enough, but I can't find a satisfactory way to set them up and prove them in lean.

A couple of years ago, Bryan Chen formalized a number of results about matroids in lean: see https://github.com/bryangingechen/lean-matroids . He started from a different, equivalent definition of matroids that does not involve a function, but encoded the above definition towards the end of his file, defining a matroid structure (paraphrased) as follows:

structure matroid (E : finset α) :=
(r (X : finset α) (hX : X ⊆ E) :  ℕ )

(R1 {X : finset α} (hX : X ⊆ E) : r X hX ≤ card X)

(R2 {X Y : finset α} (hXY : X ⊆ Y) (hY : Y ⊆ E) :
 r X (subset.trans hXY hY) ≤ r Y hY)

(R3 {X Y : finset α} (hX : X ⊆ E) (hY : Y ⊆ E) :
r (X ∪ Y) (union_subset hX hY) + r (X ∩ Y) (inter_subset hX hY) ≤ r X hX + r Y hY)

This definition works. One can go ahead and define deletion, contraction and duality, and prove all of the claims I made above without too much trouble. However, the proofs are long, and the main reason is the requirement that every evaluation of the rank function at a set X, or invocation of the axioms, must be accompanied by a proof that X ⊆ E. This requires a massive amount of bookkeeping. A typical proof will contain many rank evaluations on different sets (defined by intersections, unions, differences, etc) often on multiple different matroids with interrelated ground sets. The fact that all rank evaluations are well-defined is invariably obvious, but keeping track of all the relevant proofs gets very unwieldy. I have persisted with this for 500+ lines, formalizing a modest chunk of the basic theory, and it is painful. Bryan has told me he had a similar experience.

The solution to this seems to be to use types. Bryan also started to do this in the 'fintype2' branch of his git, but didn't get as far as the rank axioms. The idea is presumably to use the ground set E as a fintype, and think of the rank function as mapping finset E to ℕ. Here is an attempt.

variables (E: Type*) [decidable_eq E] [fintype E]

structure matroid :=
(r : finset E → ℕ)
(R1 : ∀ (X : finset E), r X ≤ card X )
(R2 : ∀ (X Y: finset E), X ⊆ Y → r X ≤ r Y)
(R3 : ∀ (X Y: finset  E), r (X ∪ Y) + r (X ∩ Y) ≤ r X + r Y)

#check finset.subtype.fintype

def submatroid (M : matroid E) (F : finset E) : matroid ( ??? ) :=
{ r := sorry,
R1 := sorry,
R2 := sorry,
R3 := sorry,
}

As you can see, I don't see how to proceed from here, even with the most basic definitions. I am hoping there is a sensible way to fill in the ??? and the sorrys so that submatroid captures the restriction of r to the subset F, together with the proofs that the three axioms are satisfied. Given that these proofs are all mathematically trivial, I would ideally like a solution that reflects this, and doesn't heavily use coercions or the like.

However, even if this is possible, I'm a little put off; here there seems to be an artificial distiction made between the 'ground set' E, which is encoded as a fintype, and its subset F, which is encoded a a set. Ideally, I would like to treat E as a set like any other inside proofs, and likewise to not have to pay due to the artificial distiction between a set F as being both the 'universe' of a submatroid and simply a subset of E. Too much of this will certainly cause problems in proofs later on that involve things like infinite classes of matroids on overlapping ground sets with many different rank functions.

I don't know if I'm asking too much, but what I am doing does seem mathematically natural enough that an elegant solution should be possible in lean. This seems like it should be analogous to issues arising in areas like algebra and topology, but from what I can tell, the finiteness causes new issues. One approach I considered with a friend is to use set E rather than finset E which made some things a little smoother but caused decidability problems with cardinalities.

If you're still reading, thank you for getting this far! Please let me know any thoughts you may have.

[Johan Commelin]

@Bryan Gin-ge Chen Did some stuff with matroids, I think

[Peter Nelson]

Yes, I have discussed this with him and linked his contribution in my post.

[Kenny Lau]

This is a tricky problem indeed. The issue is that the coercion from finset to type is not very smooth (one has to write (\u s : set E) to coerce s to a set E and then Lean can automatically coerce this to a type).

[Mario Carneiro]

The discussions about fincard would seem to be relevant here. I certainly agree that the partial function (r (X : finset α) (hX : X ⊆ E) : ℕ) is a bad idea - in fact I'm probably one of the voices behind Brian's decision to do the 'fintype2' version. But I think it would be smoother to use set E instead of finset E in the revised definition, as in (r : set E → ℕ). The main issue with doing this to begin with is that card X won't typecheck, but fincard solves that, since it has the type fincard : Sort* → ℕ it is very easy to use on basically anything.

[Mario Carneiro]

I'm referring to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finiteness

[Bryan Gin-ge Chen]

(In case it's of interest, here's a thread where I discuss some issues with defining matroid restriction on my fintype branch.)

[Kenny Lau]

import data.finset

noncomputable theory
open_locale classical
open finset

variables (E : Type*)

structure matroid :=
(r : finset E → ℕ)
(R1 : ∀ (X : finset E), r X ≤ X.card)
(R2 : ∀ {X Y : finset E}, X ⊆ Y → r X ≤ r Y)
(R3 : ∀ {X Y : finset E}, r (X ∪ Y) + r (X ∩ Y) ≤ r X + r Y)

def submatroid (M : matroid E) (F : set E) : matroid F :=
{ r := λ s, M.r $ s.image coe,
  R1 := λ s, le_trans (M.R1 _) card_image_le,
  R2 := λ s₁ s₂ hs, M.R2 $ image_subset_image hs,
  R3 := λ s₁ s₂, by { rw [image_union, image_inter], apply M.R3, exact λ _ _, subtype.ext } }

[Kenny Lau]

how is this?

[Kenny Lau]

for some weird reason I can't make the argument of R1 implicit

[Kenny Lau]

or else le_trans M.R1 card_image_le fails

[Kevin Buzzard]

There is a fincard branch but no PR yet btw

[Mario Carneiro]

implicit arguments don't work on structure fields for reasons I haven't bothered to investigate. This is one of the reasons that we often restate axioms after the structure

[Mario Carneiro]

it's generally better to just use (R1 : ∀ X : finset E, r X ≤ X.card) in the fields because it's less confusing

[Kenny Lau]

@Peter Nelson btw, if you don't plan on having more than one matroids on any type, it might be better to make it a class instead of a structure

[Peter Nelson]

Kenny Lau said:

Peter Nelson btw, if you don't plan on having more than one matroids on any type, it might be better to make it a class instead of a structure

I do need to have multiple matroids on the same type - the dual matroid (discussed near the top) is one reason why.

[Peter Nelson]

Kenny Lau said:

import data.finset

noncomputable theory
open_locale classical
open finset

variables (E : Type*)

structure matroid :=
(r : finset E → ℕ)
(R1 : ∀ (X : finset E), r X ≤ X.card)
(R2 : ∀ {X Y : finset E}, X ⊆ Y → r X ≤ r Y)
(R3 : ∀ {X Y : finset E}, r (X ∪ Y) + r (X ∩ Y) ≤ r X + r Y)

def submatroid (M : matroid E) (F : set E) : matroid F :=
{ r := λ s, M.r $ s.image coe,
  R1 := λ s, le_trans (M.R1 _) card_image_le,
  R2 := λ s₁ s₂ hs, M.R2 $ image_subset_image hs,
  R3 := λ s₁ s₂, by { rw [image_union, image_inter], apply M.R3, exact λ _ _, subtype.ext } }

I have a naive question that is more about the coding than the math - how is matroid F valid code, where the definition of matroid itself has no arguments, and how do the subsequent lambdas infer that s refers to a subset of F?

[Alex J. Best]

The argument E is a variable on the line above, so it is equivalent to structure matroid (E : Type*) :=

[Alex J. Best]

So lean will try and turn F into a Type, this will be the corresponding subtype to the set E.

[Alex J. Best]

If you open it in vscode there will probably be some coercion up arrow before F.

[Mario Carneiro]

I also find it interesting in kenny's code that the matroid is not finite but all the operations still make sense

[Peter Nelson]

Yes, one can do some things with infinite matroids - however, they break down under duality, at least when defined in terms of the rank function, since the dual rank function includes a cardinality term.

[Mario Carneiro]

I don't know the theory you are talking about, so I don't know what duality should mean here, but it sounds like maybe the fintype assumption should be introduced some time after the definition

[Mario Carneiro]

it's generally good practice to introduce assumptions when they become necessary to state and prove things, and not before

[Peter Nelson]

I would prefer if the finiteness were baked in - the reason is that if you just define an infinite matroid as an infinite set satisfying the rank axioms, you don't have the full generality of infinite matroids, which really should allow sets of infinite rank as well. The right way to talk about infinite matroids is with a completely different definition.

[Mario Carneiro]

I realize this is the mathematically natural thing to do, but it has no formalization advantage

[Peter Nelson]

I see, that makes sense.

[Kevin Buzzard]

It's like saying "I know y=f(x) is a function of x only, but let's define a new function F(x,a)=f(x) which ignores a". This is all over mathlib. For example the real square root function doesn't ask that the input is nonnegative. The assumptions which makes things sane are in the theorems not the definitions.

[Mario Carneiro]

with f(x) you know, syntactically, that it doesn't depend on a. With f(x,a) you have a theorem to prove, and apply in lots of places, and this is just added headache

[Peter Nelson]

This is all quite a paradigm shift in my head. I'm having a blast doing this stuff, though!

[Kenny Lau]

I guess the easiest example is how division is defined for every element in a field -- with a / 0 = 0 for all a

[Mario Carneiro]

the thing that surprised me about kenny's definition is that it's actually not total nonsense for infinite types. My fincard suggestion would have been nonsense for infinite types because fincard X = 0 when X is infinite

[Mario Carneiro]

it's maybe not the ideal infinite matroid type but it's still relatively well defined, which means that a lot of theorems will nevertheless apply in the infinite case

[Bryan Gin-ge Chen]

One thing I didn't realize when I was formalizing the rank in my repo was how important it was to choose good definitions for formalization.

Oxley defines the rank of a matroid (defined via the independent set axioms) as the cardinality of a basis and then defines the rank of a subset of the ground set as the rank of the submatroid created by restricting to that subset. I probably would've gotten less stuck if I had put off defining restriction and submatroids and instead simply defined the rank of a subset to be the cardinality of the maximal independent set contained in that subset. (Of course, restriction and submatroids are important concepts in their own right, but it's not clear that they're absolutely essential to the notion of rank.)

In math, switching between these two is somehow completely transparent, but when formalizing, making sure that the extra layers of definitions are easy to work with and have a nice "API" can be very difficult (particularly for newcomers like me!)

[Peter Nelson]

Yes - different matroid people have their own favourite axiom sets, but I (humbly) think that the rank function is the most powerful for formalization because it can reduce case analysis to a simple verification of linear inequalities

[Kyle Miller]

Matroids/submatroids seem to have the same issue that graphs/subgraphs have, what I was calling the "synecdoche problem" in a topic on #general.

A matroid has two things that can vary, the E type and the rank function. You don't want to define a class on E because the rank function can vary, so a matroid is best as a structure. However, you want a submatroid to be a matroid, too, and it would be nice to have a type submatroid M of submatroids for M a matroid (probably where all the matroid deletions live).

You might take a look at the mathlib:simple_graphs2 branch, where I'm experimenting with a solution to this problem for simple graphs. I think the technique works really well so far, with the only cost being that to introduce an abstract simple graph you need three things rather than two:

variables {α : Type*} (G : α) [simple_graph G]

[Kyle Miller]

Graphs and matroids are very similar, so I suspect a good solution to either will be good for the other.

[Peter Nelson]

Yes, I agree

[Bryan Gin-ge Chen]

(Here's the thread on synecdoche).

[Kyle Miller]

I posted about some of the design on #graph theory (a private stream anyone can be added to). I'll repost it here:

The definition in the simple_graphs2 branch sort of came out of the following design process. Let's say you started with this definition of a simple graph:

structure simple_graph (V : Type*) :=
(adj : V → V → Prop)
(symm : symmetric adj)
(loopless : irreflexive adj)

and then you define spanning subgraphs on a given graph (i.e., subgraphs with all the vertices) by something like

structure spanning_subgraph {V : Type*} (G : simple_graph V) :=
(adj : V → V → Prop)
(symm : symmetric adj)
(prop : ∀ (v w : V), adj v w → G.adj v w)

One basic definition for simple graphs is the set of neighboring vertices:

def neighbor_set {V : Type*} (G : simple_graph V) (v : V) := set_of (G.adj v)

However, if you have a spanning_subgraph G, you cannot use neighbor_set directly -- you would need some coercion. Let's define an interface for this. While you could try using has_coe, there is a typeclass inference problem: has_coe a b is a function of both a and b, so you would need to specify type hints to get it to coerce correctly (plus, we won't gain any benefits from Lean's automatic coercion features). This is not so bad for spanning subgraphs, but it is not so good for subgraphs since the vertex type needs to be referred to as the vertex subset coerced to a type. To make it so b is a function of a, we can define our own coercion class:

class has_coe_to_simple_graph (α : Type*) :=
(V : α → Type v)
(to_simple_graph : Π (G : α), simple_graph (V G))

Then, for example,

instance {V : Type*} (G : simple_graph V) :
  has_coe_to_simple_graph (spanning_subgraph G) :=
{ V := λ _, V,
  to_simple_graph := λ G',
  { adj := G'.adj,
    symm := G'.symm,
    loopless := λ x h, G.loopless x (G'.prop _ _ h) } }

However, we cannot yet do neighbor_set G' v for G' : spanning_subgraph G, since it is not literally a graph. Let's define some accessor functions to get some simple_graph fields for coerceable terms and use them to define the neighbor_set:

variables {α : Type*} [has_coe_to_simple_graph α]

def V (G : α) := has_coe_to_simple_graph.V G
def adj (G : α) := (has_coe_to_simple_graph.to_simple_graph G).adj

def neighbor_set (G : α) (v : V G) := set_of (adj G v)

While spanning_subgraph G is not a simple_graph per se, you can interact with it as if it were one.

This might be an OK interface as it is, but there is a simplification to this. If we were to take the fields of simple_graph and put them into has_coe_to_simple_graph, then we would have

class has_coe_to_simple_graph (α : Type*) :=
(V : α → Type v)
(adj : Π (G : α), V G → V G → Prop)
(symm : Π (G : α), symmetric (adj G))
(loopless : Π (G : α), irreflexive (adj G))

This is the class simple_graphs that I had mentioned last week! A weird thing about it, though, is how every field is a function. What if we lifted the G argument out? Let's also rename this class simple_graph. We would obtain

class simple_graph {α : Type*} (G : α) :=
(V : Type v)
(adj : V → V → Prop)
(symm : symmetric adj)
(loopless : irreflexive adj)

This is the definition in the simple_graphs2 branch. It is the result of flattening the coercion class and the definition of the structure. This lets us not have to redefine all the fields using accessor functions that depend on a coercion class: the members of this class are the accessor functions.

In the has_coe_to_simple_graph approach, note that to make things generic with respect to all things that are graph-like, lemmas and definitions would have to be in terms of the accessor functions anyway, so you would never refer to fields of simple_graph. Thus, you lose nothing by folding it all in and defining this simple_graph class.

One caveat is that to define a simple graph from a particular relation, you need a "tautological" instance:

structure simple_graph_on (V : Type u) :=
(rel : V → V → Prop)
(symm : symmetric rel)
(irrefl : irreflexive rel)

instance simple_graph_on.simple_graph (V : Type u) (G : simple_graph_on V) : simple_graph G :=
{ V := V,
  adj := G.rel,
  symm := G.symm,
  loopless := G.irrefl }

Another caveat is that different graphs have vertex types that are referred to differently, even if the vertex types are definitionally equal. For graphs on the same vertex type, you would probably want to use the type simple_graph_on V. One could define a bounded lattice instance for this.

[Peter Nelson]

@Kyle Miller - does your graph code handle contracting edges? That is a classic example where the wrong definitions can cause trouble

[Kyle Miller]

I haven't gotten to that part exactly, though there is some hastily written sorry'd code. I hestitate because I'm only used to edge contraction for multigraphs, which haven't been implemented yet.

[Peter Nelson]

Quick question - how do I go from a type E to the associated set?

[Anatole Dedecker]

Are you looking for docs#set.univ ?

[Bryan Gin-ge Chen]

There's also docs#finset.univ to get a finset from a fintype.

[Peter Nelson]

That's what I thought, but in @Kenny Lau 's code, I am trying to define contraction (some matroid on ground set E \ C) and I am getting a problem.

import data.finset

noncomputable theory
open_locale classical
open finset

variables (E : Type*)

structure matroid :=
(r : finset E → ℕ)
(R1 : ∀ (X : finset E), r X ≤ X.card)
(R2 : ∀ {X Y : finset E}, X ⊆ Y → r X ≤ r Y)
(R3 : ∀ {X Y : finset E}, r (X ∪ Y) + r (X ∩ Y) ≤ r X + r Y)

def submatroid (M : matroid E) (F : set E) : matroid F :=
{ r := λ s, M.r $ s.image coe,
  R1 := λ s, le_trans (M.R1 _) card_image_le,
  R2 := λ s₁ s₂ hs, M.R2 $ image_subset_image hs,
  R3 := λ s₁ s₂, by { rw [image_union, image_inter], apply M.R3, exact λ _ _, subtype.ext } }

Now I want to add the line

def contraction (M: matroid E) (C : set E) : matroid ( (set.univ E) \ C) := {... foo ...}

But the argument of the second matroid gives a type mismatch error. I can't see why I can't get away with the above where the F works fine in Kenny's code.

[Kenny Lau]

set.univ does not have explicit arguments (I think the error message tells you this)

[Kenny Lau]

also we prefer C\^c for complement of C

[Kyle Miller]

Here's a variation in the design space. You have a matroid_on structure for matroids on a specific E type, and then you have a matroids class that gives terms of a type the structure of a matroid -- it could also be called the unwieldy has_coe_to_matroid. Then you define accessor functions that, for {α : Type v} [matroids α], give you the fields of the term's matroid structure. Then you prove statements about matroids M : α.

I gave an implementation of submatroids and a partial implementation of contracted matroids following this pattern. (There are many missing simp lemmas that make this more useable.) Having a separate type for matroid contractions of a given matroid might seem odd, but maybe it's useful to formalize that contracted matroids are in correspondence to submatroids of the dual (I don't actually know matroid theory -- fill in the correct statement if there is one :smile:)

import data.fintype.basic
import data.finset

noncomputable theory
open_locale classical
open finset

universes u v

structure matroid_on (E : Type u) :=
(r : finset E → ℕ)
(R1 : ∀ (X : finset E), r X ≤ X.card)
(R2 : ∀ {X Y : finset E}, X ⊆ Y → r X ≤ r Y)
(R3 : ∀ (X Y : finset E), r (X ∪ Y) + r (X ∩ Y) ≤ r X + r Y)

class matroids (α : Type v) :=
(E : α → Type u)
(to_matroid : Π (M : α), matroid_on (E M))

instance matroid_on.matroids (E : Type u) : matroids (matroid_on E) :=
{ E := λ _, E,
  to_matroid := id }

namespace matroid

variables {α : Type v} [matroids α]
-- Accessor functions for terms that have a matroid representation
def E (M : α) := matroids.E M
def r {M : α} (X : finset (E M)) : ℕ := (matroids.to_matroid M).r X
def R1 (M : α) (X : finset (E M)) : r X ≤ X.card := (matroids.to_matroid M).R1 X
def R2 (M : α) {X Y : finset (E M)} (h : X ⊆ Y) : r X ≤ r Y := (matroids.to_matroid M).R2 h
def R3 (M : α) (X Y : finset (E M)) : r (X ∪ Y) + r (X ∩ Y) ≤ r X + r Y := (matroids.to_matroid M).R3 X Y

structure submatroid (M : α) :=
(F : set (E M))

def delete (M : α) (F : set (E M)) : submatroid M :=
submatroid.mk F

instance submatroid.matroid (M : α) : matroids (submatroid M) :=
{ E := λ M', M'.F,
  to_matroid := λ M',
  { r := λ s, r (s.image subtype.val),
    R1 := λ s, le_trans (R1 M _) card_image_le,
    R2 := λ s₁ s₂ hs, R2 M (image_subset_image hs),
    R3 := λ s₁ s₂, by { rw [image_union, image_inter], apply R3 M, apply subtype.ext, } } }

structure matroid_contraction (M : α) :=
(C : finset (E M))

def contract (M : α) (C : finset (E M)) : matroid_contraction M :=
matroid_contraction.mk C

instance matroid_contraction.matroid (M : α) : matroids (matroid_contraction M) :=
{ E := λ M', ↥((↑M'.C : set (E M))ᶜ),
  to_matroid := λ M',
  { r := λ s, r (s.image subtype.val ∪ M'.C) - r M'.C,
    R1 := λ s, begin
      convert_to _ ≤ (s.image subtype.val).card, symmetry,
      apply card_image_of_injective, apply subtype.val_injective,
      have h : disjoint (s.image subtype.val) M'.C,
      { intros x h, simp at h, rcases h with ⟨⟨h₁, h₂⟩, h₃⟩,
        simp at h₁, exfalso, exact h₁ h₃, },
      sorry,
    end,
    R2 := sorry,
    R3 := sorry, } }

end matroid

[Kyle Miller]

For those who are somewhat familiar with the definition of simple graphs in mathlib:simple_graphs2, I'd appreciate any thoughts you might have in comparing these two patterns. They feel pretty much the same to use, but with the above you speak of an arbitrary matroid using

variables {α : Type v} [matroids α] (M : α)

but with the mathlib:simple_graphs2 approach, you'd speak of an arbitrary matroid using

variables {α : Type v} (M : α) [matroid M]

The first approach opens you up to the possibility of extending the matroids typeclass to add additional constraints to either the matroids, or even doing wild stuff like putting a topology on α and saying how the matroid structures are continuously defined (as a made-up example).

[Kyle Miller]

And, by the way, if Lean had a way to let you prove things about matroid_on and have them automatically apply to anything with the matroids coercion typeclass, then there would be different design considerations here.

[Peter Nelson]

I really like this, @Kyle Miller - it feels very natural to be able to extract either the ground set E or the rank function r from a given matroid M, and to have the ground set implemented as a finset rather than a type. (I think) because I am new to the syntax of lean, I don't understand the reason for having a separate structure just for contractions. Will it be possible when using this code to consider a matroid and to not care that it happened to arise from a contraction?

[Kyle Miller]

@Peter Nelson I'm not sure what you are referring to exactly when you say "it feels very natural [...] to have the ground set implemented as a finset rather than a type," since the implementation above is using a type for E M, so maybe you're speaking from your other experiences.

For the type of contractions, I imagined you might have the following sort of statement (if it's true! I'm just guessing):

def dual (M : α) [fintype (E M)] : matroid_on (E M) :=
{ r := λ s, r (univ.filter (λ x, x ∉ s)) + s.card - r (univ : finset (E M)),
  R1 := sorry,
  R2 := sorry,
  R3 := sorry }

def dual_equiv (M : α) [fintype (E M)] : matroid_contraction M ≃ submatroid (dual M) := sorry

Even if there's no such statement, it is potentially useful having a matroid_contraction structure to organize proofs and definitions specifically about contractions, and it saves you from having to write ↥((↑C : set (E M))ᶜ) in lemma statements. You'll have to experiment and see, though.

Will it be possible when using this code to consider a matroid and to not care that it happened to arise from a contraction

Yes, the way the pattern works is that "consider a matroid" is written {α : Type v} [matroids α] (M : α). This lets you not care about the way in which a matroid was constructed. In a proof you can write let M' := contract M C and even though M' : matroid_contraction M, you can interact with M' as a matroid because it implements the matroids typeclass.

[Bryan Gin-ge Chen]

This lets you not care about the way in which a matroid was constructed.

Well, you still have to care that the matroid was constructed via the rank axioms as opposed to e.g. the independent set axioms.

[Peter Nelson]

Thanks, @Kyle Miller . All I meant with E is that your axioms allow me to easily access a finset that is the ground set, rather than calling it a fintype. If I weren't about to go away on holiday, I would be refactoring my code like mad with your implementation.

@Bryan Gin-ge Chen , my plan is to have the rank function as the base definition, and then prove the equivalences to the other definitions as theorems, and use defs to allow construction from circuits, indep, etc . I am not a fan of having competing types.

[Bryan Gin-ge Chen]

Yes, in hindsight I think that's probably a better way to organize things.

[Kyle Miller]

I guess with this matroids class, you can give the other definitions as structures (maybe make them protected so someone would have to go out of their way to use them), give them matroids instances, define maps from the base definition to these alternative definitions, then prove each map and the to_matroid function together form a matroid isomorphism. Lastly, you use these to pull the alternative axioms back to the base type. (I might call this design "star-shaped".) This gives precision to the statements that these other definitions are indeed equivalent.

Since they all would implement the matroids class, you could actually use the structures as the way you construct matroids using the other definitions, since they would be automatically related to the base definition. A def to do this would be superfluous at this point.