Linear Logic

Stream: Type theory

[Billy Price]

My question is really about the cases tactic and inductive definitions, but I'm making this thread to contain whatever further discussion might arise.

My expectation is that I should be able to close the first goal with cases s₂, so it realises that Ci must be Bi

ps: proof_structure
S: switching
AiBiCi: Form_occ
hA: Ai ∈ ps.form_occs
hB: Bi ∈ ps.form_occs
hC: Ci ∈ ps.form_occs
d₃: dir
s₂: steps (S (Link.ax Ai.snd Bi.snd Ai.fst)) (Link.ax Ai.snd Bi.snd Ai.fst) (Ai, tt) (Ci, d₃)
s₁: steps (S (Link.ax Ai.snd Bi.snd Ai.fst)) (Link.ax Ai.snd Bi.snd Ai.fst) (Ai, tt) (Bi, ff)
⊢ Bi = Ci ∧ ff = d₃

however when I do this, I get cases tactic failed, unsupported equality between type and constructor indices (only equalities between constructors and/or variables are supported, try cases on the indices): Ai.snd = s₂_Ai.snd

Could someone explain what this means and how to overcome it? Here's my mwe

import tactic

inductive Form : Type
| atom : ℕ → Form
| tensor : Form → Form → Form
| par : Form → Form → Form
| neg : Form → Form

infix ` ⊗ `:70 := Form.tensor
infix ` ⅋ `:65 := Form.par
prefix `~` := Form.neg

inductive Link : Type
| ax : ℕ → ℕ → Form → Link
| cut : ℕ → ℕ → Form → Link
| tensor : ℕ → ℕ → ℕ → Form → Form → Link
| par : ℕ → ℕ → ℕ → Form → Form → Link
| con : ℕ → Form → Link

def Form_occ := Form × ℕ

def is_premise (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := false
| (Link.cut n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.tensor n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.par n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.con n A) := Ai = ⟨A,n⟩

def is_conclusion (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.cut n m B) := false
| (Link.tensor n m k A B) := Ai = ⟨A ⊗ B,k⟩
| (Link.par n m k A B) := Ai = ⟨A ⅋ B,k⟩
| (Link.con n A) := false

structure proof_structure : Type :=
(links : set Link)
(form_occs : set Form_occ)
(link_prem : ∀ l ∈ links, ∀ Ai : Form_occ, is_premise Ai l → Ai ∈ form_occs)
(link_con : ∀ l ∈ links, ∀ Ai : Form_occ, is_conclusion Ai l → Ai ∈ form_occs)
(premise : Form_occ → Link)
(prem_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_premise Ai l → premise Ai = l)
(prem_range : ∀ Ai ∈ form_occs, premise Ai ∈ links ∧ is_premise Ai (premise Ai))
(conclusion : Form_occ → Link)
(con_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_conclusion Ai l → conclusion Ai = l)
(con_range : ∀ Ai ∈ form_occs, conclusion Ai ∈ links ∧ is_conclusion Ai (conclusion Ai))

@[reducible]
def dir := bool

def down := ff
def up := tt

@[reducible]
def switch := bool

def L := ff
def R := tt

def switching := Link → bool

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
| ax (Ai Bi : Form_occ) : steps (Link.ax Ai.2 Bi.2 Ai.1) ⟨Ai, up⟩ ⟨Bi, down⟩
| cut (Ai Bi : Form_occ) : steps (Link.cut Ai.2 Bi.2 Ai.1) ⟨Ai, down⟩ ⟨Bi, up⟩
| tensordown (Ai Bi Ci : Form_occ) :
  steps (Link.tensor Ai.2 Bi.2 Ci.2 Ai.1 Bi.1) ⟨if T = L then Ai else Bi,down⟩ ⟨Ci,down⟩
| tensorturn (Ai Bi Ci : Form_occ) :
  steps (Link.tensor Ai.2 Bi.2 Ci.2 Ai.1 Bi.1) ⟨if T = L then Bi else Ai,down⟩ ⟨if T = L then Ai else Bi,up⟩
| tensorup (Ai Bi Ci : Form_occ) :
  steps (Link.tensor Ai.2 Bi.2 Ci.2 Ai.1 Bi.1) ⟨Ci,up⟩ ⟨if T = L then Bi else Ai,up⟩
| pardown (Ai Bi Ci : Form_occ) :
  steps (Link.par Ai.2 Bi.2 Ci.2 Ai.1 Bi.1) ⟨if T = L then Ai else Bi,down⟩ ⟨Ci,down⟩
| parturn (Ai Bi Ci : Form_occ) :
  steps (Link.par Ai.2 Bi.2 Ci.2 Ai.1 Bi.1) ⟨if T = L then Bi else Ai,down⟩ ⟨if T = L then Bi else Ai,up⟩
| parup (Ai Bi Ci : Form_occ) :
  steps (Link.par Ai.2 Bi.2 Ci.2 Ai.1 Bi.1) ⟨Ci,up⟩ ⟨if T = L then Ai else Bi,up⟩

def step_link (ps : proof_structure) (Ai : Form_occ) (d : dir) : Link :=
if d = up
then ps.conclusion Ai
else ps.premise Ai

theorem steps_unique_prev (ps : proof_structure) (S : switching) : ∀ (Ai Bi Ci ∈ ps.form_occs), ∀ (d₁ d₂ d₃ : dir),
  steps (S (step_link ps Ai d₁)) (step_link ps Ai d₁) ⟨Ai,d₁⟩ ⟨Bi,d₂⟩ →
  steps (S (step_link ps Ai d₁)) (step_link ps Ai d₁) ⟨Ai,d₁⟩ ⟨Ci,d₃⟩ →
  Bi = Ci ∧ d₂ = d₃ :=
begin
  intros Ai Bi Ci hA hB hC d₁ d₂ d₃ s₁ s₂,
  cases (step_link ps Ai d₁),
  cases s₁,
  cases s₂,

end

[Mario Carneiro]

This is being caused by the use of steps (Link.tensor Ai.2 Bi.2 Ci.2 Ai.1 Bi.1) et al in your steps inductive

[Mario Carneiro]

the easiest way to fix it is to case split Ai Bi Ci in your lemma first

[Billy Price]

Oh the Ai.1 stuff?

[Mario Carneiro]

yes

[Billy Price]

Could you explain why Lean is complaining about that - what equality is not supported?

[Mario Carneiro]

when you do two cases in a row like this, lean has to figure out which step combinations are impossible because of incompatible indices, and that means that when the indices are complicated functions you can get this unhelpful error

[Billy Price]

indices meaning any argument to an inductive constructor?

[Mario Carneiro]

here's a simpler example:

constant f : ℕ → ℕ
inductive foo : ℕ → Prop
| zero : foo 0
| foo (n) : foo (f n)

example (a) (h1 h2 : foo a) : false :=
begin
  cases h1,
  cases h2,
end

[Mario Carneiro]

you get the same error without the zero constructor, that might be easier

[Mario Carneiro]

constant f : ℕ → ℕ
inductive foo : ℕ → Prop
| foo (n) : foo (f n)

example (a) (h1 h2 : foo a) : false :=
begin
  cases h1 with n,
  cases h2 with m,
end

cases tactic failed, unsupported equality between type and constructor indices
(only equalities between constructors and/or variables are supported, try cases on the indices):
f n = f m

[Mario Carneiro]

the problem is that cases wants to prove that both cases apply, so a has to equal f n and also f m, so f n = f m, but rather than putting this equality in your context it assumes that the equality can be eliminated by using injectivity of constructors. That is often the case, for example if I do the same thing with 0 and +1:

inductive foo : ℕ → Prop
| zero : foo 0
| foo (n) : foo (n + 1)

example (a) (h1 h2 : foo a) : false :=
begin
  cases h1 with n;
  cases h2 with m,
  -- two cases generated, and in the second case we only have one `n`,
  -- because `n + 1 = m + 1` was used to derive `n = m` and eliminate `m`
end

But in general the index can be an arbitrary function and in that case you get that error

[Billy Price]

hmm, I'm a little confused by the constructor also being called foo - is that overloading?

[Mario Carneiro]

Oh it doesn't really matter. They are in different namespaces, the constructor is called foo.foo

[Billy Price]

gotcha

[Mario Carneiro]

A general way to avoid the issue and explicitly receive equality assumptions instead of letting cases try and fail to discharge them is to use generalize or generalize_hyp to replace the problematic subterms with fresh variables

begin
  intros Ai Bi Ci hA hB hC d₁ d₂ d₃ s₁ s₂,
  cases (step_link ps Ai d₁),
  cases s₁,
  generalize_hyp eA1 : Ai.1 = Ai1 at s₂,
  generalize_hyp eA2 : Ai.2 = Ai2 at s₂,
  generalize_hyp eB2 : Bi.2 = Bi2 at s₂,
  cases s₂; try { cases eA1 }; try { cases eA2 }; try { cases eB2 },
end

The cases eA1 step tries to eliminate the equality the same way cases normally would, but since it's in a try block it will simply leave the equality in the context if it failed to eliminate it

[Mario Carneiro]

looking at the resulting subgoals, the only failure was eB2: Bi.snd = Ci.snd in the first subgoal

[Mario Carneiro]

which can't be eliminated by cases unless you pattern match Bi and Ci first

[Billy Price]

(deleted)

[Billy Price]

(deleted)

[Billy Price]

It would be nice to not have to destruct the Ai's every time I want to prove something, but the need for Ai.1 traces back to the definition of a link. For example I can't just make it Link.tensor : Form_occ -> Form_occ -> Form_occ -> Link because I need the third Form_occ to have a formula which is the tensor of the first two.

[Billy Price]

and if I do Link.tensor : Form_occ -> Form_occ -> Link then I'm missing the index that accompanies the tensored formula. Is there a better way to implement this?

[Mario Carneiro]

Another way to avoid the need to generalize all the time is to bake additional variables into the inductive constructor:

| tensordown (A B C : Form) (ai bi ci : ℕ) :
  steps (Link.tensor ai bi ci A B) ⟨if T = L then (A, ai) else (B, bi),down⟩ ⟨(C, ci),down⟩

[Mario Carneiro]

I don't really understand the role of Form_occ here

[Mario Carneiro]

what does the nat mean?

[Mario Carneiro]

Do you have a more mathematical presentation of this logic?

[Billy Price]

This is Girard's proof nets. It's a graph of formula occurrences (the same formula can appear distinctly) connected by edges which are each part of a tensor, par, axiom or cut link. A link is really a subgraph containing 2-3 formulas and 1-2 edges. There are other definitions but here is what I'm trying to stay truest to https://williamtroiani.github.io/pdfs/Proof-nets.pdf

[Billy Price]

Here's what the proof net "looks like"
image.png
You can ignore the blue lines (they are a path around the proof net I'm defining later), and the dotted lines indicate what switching is associated to the link. The links are implicit as subgraphs here, but I think that's hard to formalise, hence the definition "a proof structure is a set of formula occurrences and a set of links", where a link is explicitly the data of the associated formula occurences in the subgraph, and the actual edges of the intended graph are implicit in the definition

[Mario Carneiro]

I see, so this is more of a directed graph than an inductive proof object in the traditional sense

[Mario Carneiro]

and the Form_occs are nodes in the graph

[Billy Price]

yeah

[Mario Carneiro]

So what does steps correspond to in that document? It looks kind of like the "multiplicative proof structure" 1.0.9 but dir and T : switch look different

[Billy Price]

Oh steps describes the flow of the path around a proof structure. In the example picture, if you start at "down on A", the next step must be "down on A ox B", since A is the premise of a tensor link and the switching of that tensor link is L.

[Billy Price]

See 2.0.2

[Billy Price]

Then a path is a list of formulas paired with ups and downs, such that each sequential pair satisfies steps

[Billy Price]

I could define it as a function from the current "step" to the next - not sure what's better.

[Mario Carneiro]

hm, I don't have any much better suggestion than having steps like

| tensordown (A B C : Form) (ai bi ci : ℕ) :
  steps (Link.tensor ai bi ci A B) ⟨if T = L then (A, ai) else (B, bi),down⟩ ⟨(C, ci),down⟩

although you can also factor out the tensor steps like so, to keep the Form_occ encapsulated:

inductive steps_tensor (T : switch) (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor ⟨if T = L then Ai else Bi,down⟩ ⟨Ci,down⟩
| turn : steps_tensor ⟨if T = L then Bi else Ai,down⟩ ⟨if T = L then Ai else Bi,up⟩
| up : steps_tensor ⟨Ci,up⟩ ⟨if T = L then Bi else Ai,up⟩

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
...
| tensor (A B C : Form) (ai bi ci : ℕ) (x y) :
  steps_tensor T (A, ai) (B, bi) (A ⊗ B, ci) x y → steps (Link.tensor ai bi ci A B) x y

[Mario Carneiro]

you can even factor out the switching like so:

inductive steps_tensor (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor ⟨Ai,down⟩ ⟨Ci,down⟩
| turn : steps_tensor ⟨Bi,down⟩ ⟨Ai,up⟩
| up : steps_tensor ⟨Ci,up⟩ ⟨Bi,up⟩

| tensor_L (A B C : Form) (ai bi ci : ℕ) (x y) :
  T = L → steps_tensor (A, ai) (B, bi) (A ⊗ B, ci) x y →
  steps (Link.tensor ai bi ci A B) x y
| tensor_R (A B C : Form) (ai bi ci : ℕ) (x y) :
  T = R → steps_tensor (B, bi) (A, ai) (A ⊗ B, ci) x y →
  steps (Link.tensor ai bi ci A B) x y

[Mario Carneiro]

that last one is a bit more convenient if T is an index of the inductive type:

inductive steps : switch → Link → Form_occ × dir → Form_occ × dir → Prop
...
| tensor_L (A B C : Form) (ai bi ci : ℕ) (x y) :
  steps_tensor (A, ai) (B, bi) (A ⊗ B, ci) x y →
  steps L (Link.tensor ai bi ci A B) x y
| tensor_R (A B C : Form) (ai bi ci : ℕ) (x y) :
  steps_tensor (B, bi) (A, ai) (A ⊗ B, ci) x y →
  steps R (Link.tensor ai bi ci A B) x y

[Mario Carneiro]

Here's a full version with those refactorings. I renamed steps_tensor to routing because steps_par is the same thing

inductive routing (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : routing ⟨Ai,down⟩ ⟨Ci,down⟩
| turn : routing ⟨Bi,down⟩ ⟨Ai,up⟩
| up : routing ⟨Ci,up⟩ ⟨Bi,up⟩

def switch.flip {α β} (f : α → α → β) : switch → α → α → β
| L a b := f a b
| R a b := f b a

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
| ax (Ai Bi : Form_occ) : steps (Link.ax Ai.2 Bi.2 Ai.1) ⟨Ai, up⟩ ⟨Bi, down⟩
| cut (Ai Bi : Form_occ) : steps (Link.cut Ai.2 Bi.2 Ai.1) ⟨Ai, down⟩ ⟨Bi, up⟩
| tensor (A B C : Form) (ai bi ci : ℕ) (x y) :
  T.flip routing (A, ai) (B, bi) (A ⊗ B, ci) x y →
  steps (Link.tensor ai bi ci A B) x y
| par (A B C : Form) (ai bi ci : ℕ) (x y) :
  T.flip routing (A, ai) (B, bi) (A ⅋ B, ci) x y →
  steps (Link.par ai bi ci A B) x y

[Billy Price]

ooh I like that

[Billy Price]

steps_par is different to steps_tensor in the up and turn cases

[Mario Carneiro]

oh, like this:

inductive steps_tensor (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor ⟨Ai,down⟩ ⟨Ci,down⟩
| turn : steps_tensor ⟨Bi,down⟩ ⟨Ai,up⟩
| up : steps_tensor ⟨Ci,up⟩ ⟨Bi,up⟩

inductive steps_par (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_par ⟨Ai,down⟩ ⟨Ci,down⟩
| turn : steps_par ⟨Bi,down⟩ ⟨Bi,up⟩
| up : steps_par ⟨Ci,up⟩ ⟨Ai,up⟩

[Mario Carneiro]

I think you can still use switch.flip to get the L and R versions though

[Billy Price]

are you saying steps_par could be defined using steps_tensor and switch.flip?

[Mario Carneiro]

no, I only mean that steps_par in the L and R case is correctly constructed by conditionally flipping the Ai and Bi inputs

[Billy Price]

ah yep

[Billy Price]

Cheers, I really like this refactoring!

[Mario Carneiro]

I didn't touch the ax and cut constructors, you probably want to use separate Form and nat parameters there

[Billy Price]

It seems like this will help break up the proof into a few shorter ones

[Mario Carneiro]

yeah that's the real power of this technique

[Billy Price]

yep, I'll see how it goes.

[Billy Price]

it doesn't like the switch.flip definition

[Billy Price]

says delete the second equation

[Mario Carneiro]

@[pattern] def L := ff
@[pattern] def R := tt

[Billy Price]

What is pattern (or where do I read about it in the docs)?

[Billy Price]

How do I make this notation appear in the goal window?

@[reducible]
def dir := bool

@[pattern] def down := ff
@[pattern] def up := tt

notation Ai`↓` := ((Ai,down) : Form_occ × dir)
notation Ai`↑` := ((Ai,up) : Form_occ × dir)

[Mario Carneiro]

@[pattern] lets the equation compiler unfold a definition when compiling a pattern match

[Billy Price]

What was it doing before to accept this as a definition?

def switch.flip {α β} (f : α → α → β) : switch → α → α → β
| L a b := f a b

[Mario Carneiro]

it thinks L is a variable

[Mario Carneiro]

def with_down (Ai : Form_occ) := (Ai,down)
def with_up (Ai : Form_occ) := (Ai,up)
postfix `↓`:max_plus := with_down
postfix `↑`:max_plus := with_up

inductive steps_tensor (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor Ai↓ Ci↓
| turn : steps_tensor Bi↓ Ai↑
| up : steps_tensor Ci↑ Bi↑

#print steps_tensor.down
-- constructor steps_tensor.down : ∀ {Ai Bi Ci : Form_occ}, steps_tensor Ai Bi Ci Ai↓ Ci↓

[Mario Carneiro]

you can also mark with_down and with_up as @[pattern]:

@[pattern] def with_down (Ai : Form_occ) := (Ai,down)
@[pattern] def with_up (Ai : Form_occ) := (Ai,up)
postfix `↓`:max_plus := with_down
postfix `↑`:max_plus := with_up

example : Form_occ × dir → true
| A↑ := trivial
| A↓ := trivial

[Billy Price]

:heart_eyes:

[Billy Price]

How do i do cases on s1 with ... when the constructor arguments vary?

[Billy Price]

like doing cases on steps T Δ X Z with this definition

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
| ax  (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.ax ai ni A) Bi↑ Ci↓
| cut (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.cut ai ni A) Bi↓ Ci↑
| con (A : Form) (ai : ℕ)            : steps (Link.con ai A) (A, ai)↓ (A,ai)↑
| tensor (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_tensor (A, ai) (B, bi) (A ⊗ B, ci) x y →
  steps (Link.tensor ai bi ci A B) x y
| par (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_par (A, ai) (B, bi) (A ⅋ B, ci) x y →
  steps (Link.par ai bi ci A B) x y

[Mario Carneiro]

I don't follow. Do you have a mwe? cases s1 with ... should work

[Billy Price]

I mean the naming of the variables, since the different constructors have different arguments.
...
Okay so when I asked the question I thought that lean's behaviour was to use the same "with"-variables for each constructor, but trying it out it actually lets you name them all in sequence? So I guess my aim is to improve on this (which does what I want, but... wtf).

theorem steps_unique_prev (T : switch) (Δ : Link) (X Y Z) : steps T Δ X Z → steps T Δ Y Z → X = Y :=
begin
  intros s₁ s₂,
  cases s₁ with A ai ni Bi Ci dBC A ai ni Bi Ci dBC A ai A B ai bi ci x y t₁ A B ai bi ci x y p₁,
end

[Billy Price]

mwe

import tactic

inductive Form : Type
| atom : ℕ → Form
| tensor : Form → Form → Form
| par : Form → Form → Form
| neg : Form → Form

infix ` ⊗ `:70 := Form.tensor
infix ` ⅋ `:65 := Form.par
prefix `~` := Form.neg

inductive Link : Type
| ax : ℕ → ℕ → Form → Link
| cut : ℕ → ℕ → Form → Link
| tensor : ℕ → ℕ → ℕ → Form → Form → Link
| par : ℕ → ℕ → ℕ → Form → Form → Link
| con : ℕ → Form → Link

def Form_occ := Form × ℕ

def is_premise (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := false
| (Link.cut n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.tensor n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.par n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.con n A) := Ai = ⟨A,n⟩

def is_conclusion (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.cut n m B) := false
| (Link.tensor n m k A B) := Ai = ⟨A ⊗ B,k⟩
| (Link.par n m k A B) := Ai = ⟨A ⅋ B,k⟩
| (Link.con n A) := false

structure proof_structure : Type :=
(links : set Link)
(form_occs : set Form_occ)
(link_prem : ∀ l ∈ links, ∀ Ai : Form_occ, is_premise Ai l → Ai ∈ form_occs)
(link_con : ∀ l ∈ links, ∀ Ai : Form_occ, is_conclusion Ai l → Ai ∈ form_occs)
(premise : Form_occ → Link)
(prem_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_premise Ai l → premise Ai = l)
(prem_range : ∀ Ai ∈ form_occs, premise Ai ∈ links ∧ is_premise Ai (premise Ai))
(conclusion : Form_occ → Link)
(con_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_conclusion Ai l → conclusion Ai = l)
(con_range : ∀ Ai ∈ form_occs, conclusion Ai ∈ links ∧ is_conclusion Ai (conclusion Ai))

@[reducible]
def dir := bool

@[pattern] def down := ff
@[pattern] def up := tt

@[pattern] def with_down (Ai : Form_occ) := (Ai,down)
@[pattern] def with_up (Ai : Form_occ) := (Ai,up)
postfix `↓`:max_plus := with_down
postfix `↑`:max_plus := with_up

@[reducible]
def switch := bool

@[pattern] def L := ff
@[pattern] def R := tt

def switching := Link → switch

def switch.flip {α β} (f : α → α → β) : switch → α → α → β
| L a b := f a b
| R a b := f b a

inductive steps_tensor (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor Ai↓ Ci↓
| turn : steps_tensor Bi↓ Ai↑
| up : steps_tensor Ci↑ Bi↑

inductive steps_par (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_par Ai↓ Ci↓
| turn : steps_par Bi↓ Bi↑
| up : steps_par Ci↑ Ai↑

inductive dual (A : Form) (ai ni : ℕ) : Form_occ → Form_occ → Prop
| posneg : dual (A,ai) (~A,ni)
| negpos : dual (~A,ni) (A,ai)

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
| ax  (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.ax ai ni A) Bi↑ Ci↓
| cut (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.cut ai ni A) Bi↓ Ci↑
| con (A : Form) (ai : ℕ)            : steps (Link.con ai A) (A, ai)↓ (A,ai)↑
| tensor (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_tensor (A, ai) (B, bi) (A ⊗ B, ci) x y →
  steps (Link.tensor ai bi ci A B) x y
| par (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_par (A, ai) (B, bi) (A ⅋ B, ci) x y →
  steps (Link.par ai bi ci A B) x y

theorem steps_unique_prev (T : switch) (Δ : Link) (X Y Z) : steps T Δ X Z → steps T Δ Y Z → X = Y :=
begin
  intros s₁ s₂,
  cases s₁ with A ai ni Bi Ci dBC A ai ni Bi Ci dBC A ai A B ai bi ci x y t₁ A B ai bi ci x y p₁,
end

[Billy Price]

Okay it's been a while since I wrote lean and I just remembered the case syntax.

[Billy Price]

I'm running into this error

cases tactic failed, when eliminating equality left-hand-side depends on right-hand-side
state:
T : switch,
A : Form,
ai ni : ℕ,
dBC : dual A ai ni (A, ai) (~A, ni),
s₁ : steps T (Link.ax ai ni A) ((A, ai), up) ((~A, ni), down),
s₂ : steps T (Link.ax ai ni A) ((~A, ni), up) ((~A, ni), down),
d₂ : dual A ai ni (~A, ni) (~A, ni)
⊢ (~A) = A → ni = ai → d₂ == dual.negpos → (A, ai) = (~A, ni)

here's my proof so far (compatible with mwe above)

theorem steps_unique_prev (T : switch) (Δ : Link) (X Y Z) : steps T Δ X Z → steps T Δ Y Z → X = Y :=
begin
  intros s₁ s₂,
  cases s₁,
  case steps.ax : A ai ni Bi Ci dBC { cases dBC, cases s₂ with _ _ _ Di _ d₂, congr, cases d₂, },
end

[Billy Price]

I completely agree with the error, i.e. that it shouldn't be able to solve (~A) = A, but then shouldn't it throw out the negpos case as a possible constructor for d₂: dual A ai ni Di (~A, ni)?

inductive dual (A : Form) (ai ni : ℕ) : Form_occ → Form_occ → Prop
| posneg : dual (A,ai) (~A,ni)
| negpos : dual (~A,ni) (A,ai)

[Mario Carneiro]

You can also use rcases instead of cases followed by case; it allows you to write all the variables at the top but grouped by constructor like rcases s1 with <A, ai, ni, Bi, Ci, dBC> | <A, ai, ni, Bi, Ci, dBC> | ...

[Mario Carneiro]

probably for an inductive as big as this case is preferable

[Mario Carneiro]

theorem dual_unique_prev {A ai ni Bi Ci Di}
  (d₁ : dual A ai ni Bi Ci) (d₂ : dual A ai ni Di Ci) : Bi = Di :=
begin
  generalize_hyp e : Ci = Ci' at d₂,
  have : A ≠ ~A,
  { intro e,
    apply_fun Form.sizeof at e,
    refine ne_of_lt _ e,
    rw [Form.sizeof, nat.add_comm], exact nat.lt_succ_self _ },
  cases d₁; cases d₂; injection e with e1 e2; cases e2;
  try { cases e1 }; [refl, cases this e1.symm, cases this e1, refl]
end

theorem steps_unique_prev (T : switch) (Δ : Link) (X Y Z) : steps T Δ X Z → steps T Δ Y Z → X = Y :=
begin
  intros s₁ s₂,
  cases s₁,
  case steps.ax : A ai ni Bi Ci dBC {
    cases s₂ with _ _ _ Di _ d₂,
    rw dual_unique_prev dBC d₂ },
end

[Billy Price]

wild - I would have expected ~A /= A to be as simple as nat.succ x /= x - or does that also require a proof like that?

[Mario Carneiro]

Billy Price said:

I completely agree with the error, i.e. that it shouldn't be able to solve (~A) = A, but then shouldn't it throw out the negpos case as a possible constructor for d₂: dual A ai ni Di (~A, ni)?

inductive dual (A : Form) (ai ni : ℕ) : Form_occ → Form_occ → Prop
| posneg : dual (A,ai) (~A,ni)
| negpos : dual (~A,ni) (A,ai)

The problem isn't that it can't solve (~A) = A, but it can't solve or refute it. It is possible to refute with a proof (the have in my proof), but this proof isn't obvious to lean

[Mario Carneiro]

The proof of ~A != A is being reduced to the proof that nat.succ x != x here

[Mario Carneiro]

I'm taking advantage of the fact that there is already a function Form.sizeof : Form -> nat such that sizeof (~A) = sizeof A + 1

[Mario Carneiro]

this function is defined automatically and used as a component in the equation compiler

[Billy Price]

oh right - but how is n /= n+1 proved?

[Mario Carneiro]

by induction

[Mario Carneiro]

you can also prove this form theorem by induction

[Billy Price]

is this not "easy" to do for any inductive type? I thought it was essentially a theorem about injectivity of inductively defined things

[Mario Carneiro]

theorem ne_neg_self : ∀ A : Form, A ≠ ~A
| (Form.neg A) e := ne_neg_self _ (Form.neg.inj e)

[Mario Carneiro]

it's not an "easy" theorem in that sense, because A shows up on both sides

[Mario Carneiro]

it's not injectivity of the constructor, for example

[Mario Carneiro]

This generalizes to theorems saying that A != ~~(A ⅋ B) ⊗ C for example, and the general proof approach uses sizeof to prove that the size of A has to be less than itself

[Billy Price]

It just seems like they could all be bowled over by some theorem saying that if f(A) = g(A) where f and g are combinations of constructors then f = g at some level between syntax and semantics.

[Billy Price]

If not a theorem then at least a tactic that does what you did

[Billy Price]

Not complaining I'm just surprised lean doesn't take care of it

[Mario Carneiro]

That's injectivity, and there are tactics for that (cases and injection)

[Billy Price]

It seems clear that that should extend to the case where f is the "identity pattern"

[Mario Carneiro]

Actually maybe I don't know what you mean

[Mario Carneiro]

what is f?

[Billy Price]

Wait isn't injectivity f(A) = f(B) => A = B? not what I wrote

[Mario Carneiro]

A tactic could do what I did, yes. It doesn't exist and it's a little hard to detect the case of interest

[Billy Price]

f is like any pattern of constructors

[Mario Carneiro]

I think this is false

[Mario Carneiro]

like A ⊗ B = B ⊗ A does not imply (\lam x, x ⊗ B) = (\lam x, B ⊗ x)

[Billy Price]

oh of course, I've gone wrong somewhere

[Mario Carneiro]

the actual theorem I'm using is that a term cannot be a strict subterm of itself

[Mario Carneiro]

and the proof is to map terms to sizes (natural numbers or other well ordered type) such that strict subterm implies strict inequality

[Mario Carneiro]

but there is no general definition of "strict subterm" in lean

[Mario Carneiro]

that would presumably be part of the aforementioned tactic

[Billy Price]

ah okay, why not? is it something to do with different expressions being the same term or something?

[Mario Carneiro]

the definition has to be created on the fly for every inductive

[Mario Carneiro]

and this particular definition is only useful if you want this acyclicity tactic; it doesn't come up in the equation compiler so no one bothered

[Billy Price]

I mean it seems clear to me that something like this could come up fairly often with cases

[Billy Price]

But I appreciate what I've got to work with. Lean is great. Thanks Mario :pray:

[Mario Carneiro]

I think this particular goal came up because of the way dual is defined

[Billy Price]

sure, but is it that an odd usage?

[Mario Carneiro]

By the way, in the notes, ~ is not an inductive constructor, it is an involution on Form

[Mario Carneiro]

so this lemma about A = ~A is not necessary because the two constructors of dual are the same

[Billy Price]

Oh yeah, I'm not following the notes in that sense because I thought it would be too complicated. My Form is the PreForm from the notes.

[Billy Price]

Though it would be more desirable to prove these things for the real formulas, not just Preforms.

[Billy Price]

If I were to do that, would it be more sensible to introduce an equivalence relation on my inductive definition of Form? Or would I make a class/structure over some abstract type with negation, tensor and par operations satisfying ~~A = A, and the de morgan laws?

[Billy Price]

How is this possible?

rewrite tactic failed, did not find instance of the pattern in the target expression
  switch.flip ?m_3 L ?m_4 ?m_5
state:
case bool.ff
X Y y : Form_occ × dir,
A B : Form,
ai bi ci : ℕ,
s₁ : steps ff (Link.tensor ai bi ci A B) X y,
t₁ : switch.flip steps_tensor ff (A, ai) (B, bi) (A ⊗ B, ci) X y,
t₂ : switch.flip steps_tensor ff (A, ai) (B, bi) (A ⊗ B, ci) Y y
⊢ X = Y

here's where I'm at - I originally tried to do simp but it wouldn't recognise it so I added flip_L and flip_R

import tactic

inductive Form : Type
| atom : ℕ → Form
| tensor : Form → Form → Form
| par : Form → Form → Form
| neg : Form → Form

infix ` ⊗ `:70 := Form.tensor
infix ` ⅋ `:65 := Form.par
prefix `~` := Form.neg

inductive Link : Type
| ax : ℕ → ℕ → Form → Link
| cut : ℕ → ℕ → Form → Link
| tensor : ℕ → ℕ → ℕ → Form → Form → Link
| par : ℕ → ℕ → ℕ → Form → Form → Link
| con : ℕ → Form → Link

def Form_occ := Form × ℕ

def is_premise (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := false
| (Link.cut n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.tensor n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.par n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.con n A) := Ai = ⟨A,n⟩

def is_conclusion (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.cut n m B) := false
| (Link.tensor n m k A B) := Ai = ⟨A ⊗ B,k⟩
| (Link.par n m k A B) := Ai = ⟨A ⅋ B,k⟩
| (Link.con n A) := false

structure proof_structure : Type :=
(links : set Link)
(form_occs : set Form_occ)
(link_prem : ∀ l ∈ links, ∀ Ai : Form_occ, is_premise Ai l → Ai ∈ form_occs)
(link_con : ∀ l ∈ links, ∀ Ai : Form_occ, is_conclusion Ai l → Ai ∈ form_occs)
(premise : Form_occ → Link)
(prem_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_premise Ai l → premise Ai = l)
(prem_range : ∀ Ai ∈ form_occs, premise Ai ∈ links ∧ is_premise Ai (premise Ai))
(conclusion : Form_occ → Link)
(con_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_conclusion Ai l → conclusion Ai = l)
(con_range : ∀ Ai ∈ form_occs, conclusion Ai ∈ links ∧ is_conclusion Ai (conclusion Ai))

@[reducible]
def dir := bool

@[pattern] def down := ff
@[pattern] def up := tt

@[pattern] def with_down (Ai : Form_occ) := (Ai,down)
@[pattern] def with_up (Ai : Form_occ) := (Ai,up)
postfix `↓`:max_plus := with_down
postfix `↑`:max_plus := with_up

@[reducible]
def switch := bool

@[pattern] def L := ff
@[pattern] def R := tt

def switching := Link → switch

@[simp]
def switch.flip {α β} (f : α → α → β) : switch → α → α → β
| L a b := f a b
| R a b := f b a

@[simp] lemma flip_L {α β} {f : α → α → β} {a b} : switch.flip f L a b = f a b := rfl
@[simp] lemma flip_R {α β} {f : α → α → β} {a b} : switch.flip f R a b = f b a := rfl

inductive steps_tensor (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor Ai↓ Ci↓
| turn : steps_tensor Bi↓ Ai↑
| up : steps_tensor Ci↑ Bi↑

inductive steps_par (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_par Ai↓ Ci↓
| turn : steps_par Bi↓ Bi↑
| up : steps_par Ci↑ Ai↑

inductive dual (A : Form) (ai ni : ℕ) : Form_occ → Form_occ → Prop
| posneg : dual (A,ai) (~A,ni)
| negpos : dual (~A,ni) (A,ai)

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
| ax  (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.ax ai ni A) Bi↑ Ci↓
| cut (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.cut ai ni A) Bi↓ Ci↑
| con (A : Form) (ai : ℕ)            : steps (Link.con ai A) (A, ai)↓ (A,ai)↑
| tensor (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_tensor (A, ai) (B, bi) (A ⊗ B, ci) x y →
  steps (Link.tensor ai bi ci A B) x y
| par (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_par (A, ai) (B, bi) (A ⅋ B, ci) x y →
  steps (Link.par ai bi ci A B) x y

theorem dual_unique_prev {A ai ni Bi Ci Di}
  (d₁ : dual A ai ni Bi Ci) (d₂ : dual A ai ni Di Ci) : Bi = Di :=
begin
  generalize_hyp e : Ci = Ci' at d₂,
  have : A ≠ ~A,
  { intro e,
    apply_fun Form.sizeof at e,
    refine ne_of_lt _ e,
    rw [Form.sizeof, nat.add_comm], exact nat.lt_succ_self _ },
  cases d₁; cases d₂; injection e with e1 e2; cases e2;
  try { cases e1 }; [refl, cases this e1.symm, cases this e1, refl]
end

theorem steps_tensor_unique_prev (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_tensor Ai Bi Ci X Z → steps_tensor Ai Bi Ci Y Z → X = Y :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_tensor_unique_next (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_tensor Ai Bi Ci X Y → steps_tensor Ai Bi Ci X Z → Y = Z :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_par_unique_prev (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_par Ai Bi Ci X Z → steps_par Ai Bi Ci Y Z → X = Y :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_par_unique_next (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_par Ai Bi Ci X Y → steps_par Ai Bi Ci X Z → Y = Z :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_unique_prev (T : switch) (Δ : Link) (X Y Z) : steps T Δ X Z → steps T Δ Y Z → X = Y :=
begin
  intros s₁ s₂,
  cases s₁,
  case steps.ax : A ai ni Bi Ci d₁ {
    cases s₂ with _ _ _ Di _ d₂,
    rw dual_unique_prev d₁ d₂ },
  case steps.cut : A ai ni Bi Ci d₁ {
    rcases s₂ with _ | ⟨_,_,_,Di,_,d₂⟩,
    rw dual_unique_prev d₂ d₁
  },
  case steps.con : A ai { cases s₂, refl },
  case steps.tensor : A B ai bi ci X y t₁ {
    rcases s₂ with _ | _ | _ | ⟨_,_,_,_,_,_,_,t₂⟩,
    cases T, rw flip_L,
  },
end

[Mario Carneiro]

well, as you can see from the goal state, t₁ : switch.flip steps_tensor ff (A, ai) (B, bi) (A ⊗ B, ci) X y, does not have L in the second argument. cases has a bad habit of reducing all indices to weak head normal form, which is why it shows up as ff instead of L. Marking L as reducible should help

[Billy Price]

Yeah I already tried removing all the L's and it's still the same problem

[Billy Price]

Also adding the reducible attribute also does nothign

[Billy Price]

import tactic

inductive Form : Type
| atom : ℕ → Form
| tensor : Form → Form → Form
| par : Form → Form → Form
| neg : Form → Form

infix ` ⊗ `:70 := Form.tensor
infix ` ⅋ `:65 := Form.par
prefix `~` := Form.neg

inductive Link : Type
| ax : ℕ → ℕ → Form → Link
| cut : ℕ → ℕ → Form → Link
| tensor : ℕ → ℕ → ℕ → Form → Form → Link
| par : ℕ → ℕ → ℕ → Form → Form → Link
| con : ℕ → Form → Link

inductive valid_link : Link → Prop
| ax  (i j A) : valid_link (Link.ax i j A)
| cut (i j A) : valid_link (Link.cut i j A)
| tensor (i j k A B) : (A,i) ≠ (B,j) → valid_link (Link.tensor i j k A B)
| par (i j k A B) : (A,i) ≠ (B,j) → valid_link (Link.par i j k A B)
| con (i A) : valid_link (Link.con i A)

def Form_occ := Form × ℕ

def is_premise (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := false
| (Link.cut n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.tensor n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.par n m k A B) := (Ai = ⟨A,n⟩) ∨ (Ai = ⟨B,m⟩)
| (Link.con n A) := Ai = ⟨A,n⟩

def is_conclusion (Ai : Form_occ) : Link → Prop
| (Link.ax n m B) := (Ai = ⟨B,n⟩) ∨ (Ai = ⟨~B,m⟩)
| (Link.cut n m B) := false
| (Link.tensor n m k A B) := Ai = ⟨A ⊗ B,k⟩
| (Link.par n m k A B) := Ai = ⟨A ⅋ B,k⟩
| (Link.con n A) := false

structure proof_structure : Type :=
(links : set Link)
(form_occs : set Form_occ)
(link_prem : ∀ l ∈ links, ∀ Ai : Form_occ, is_premise Ai l → Ai ∈ form_occs)
(link_con : ∀ l ∈ links, ∀ Ai : Form_occ, is_conclusion Ai l → Ai ∈ form_occs)
(premise : Form_occ → Link)
(prem_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_premise Ai l → premise Ai = l)
(prem_range : ∀ Ai ∈ form_occs, premise Ai ∈ links ∧ is_premise Ai (premise Ai))
(conclusion : Form_occ → Link)
(con_unique : ∀ Ai ∈ form_occs, ∀ l ∈ links, is_conclusion Ai l → conclusion Ai = l)
(con_range : ∀ Ai ∈ form_occs, conclusion Ai ∈ links ∧ is_conclusion Ai (conclusion Ai))

@[reducible]
def dir := bool

@[pattern] def down := ff
@[pattern] def up := tt

@[pattern] def with_down (Ai : Form_occ) := (Ai,down)
@[pattern] def with_up (Ai : Form_occ) := (Ai,up)
postfix `↓`:max_plus := with_down
postfix `↑`:max_plus := with_up

@[reducible]
def switch := bool

@[reducible, pattern] def L := ff
@[reducible, pattern] def R := tt

def switching := Link → switch

@[simp]
def switch.flip {α β} (f : α → α → β) : switch → α → α → β
| L a b := f a b
| R a b := f b a

@[simp] lemma flip_L {α β} {f : α → α → β} {a b} : switch.flip f L a b = f a b := rfl
@[simp] lemma flip_R {α β} {f : α → α → β} {a b} : switch.flip f R a b = f b a := rfl

inductive steps_tensor (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor Ai↓ Ci↓
| turn : steps_tensor Bi↓ Ai↑
| up : steps_tensor Ci↑ Bi↑

inductive steps_par (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_par Ai↓ Ci↓
| turn : steps_par Bi↓ Bi↑
| up : steps_par Ci↑ Ai↑

inductive dual (A : Form) (ai ni : ℕ) : Form_occ → Form_occ → Prop
| posneg : dual (A,ai) (~A,ni)
| negpos : dual (~A,ni) (A,ai)

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
| ax  (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.ax ai ni A) Bi↑ Ci↓
| cut (A : Form) (ai ni : ℕ) (Bi Ci) : dual A ai ni Bi Ci → steps (Link.cut ai ni A) Bi↓ Ci↑
| con (A : Form) (ai : ℕ)            : steps (Link.con ai A) (A, ai)↓ (A,ai)↑
| tensor (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_tensor (A, ai) (B, bi) (A ⊗ B, ci) x y →
  steps (Link.tensor ai bi ci A B) x y
| par (A B : Form) (ai bi ci : ℕ) (x y) :
  T.flip steps_par (A, ai) (B, bi) (A ⅋ B, ci) x y →
  steps (Link.par ai bi ci A B) x y

theorem dual_unique_prev {A ai ni Bi Ci Di}
  (d₁ : dual A ai ni Bi Ci) (d₂ : dual A ai ni Di Ci) : Bi = Di :=
begin
  generalize_hyp e : Ci = Ci' at d₂,
  have : A ≠ ~A,
  { intro e,
    apply_fun Form.sizeof at e,
    refine ne_of_lt _ e,
    rw [Form.sizeof, nat.add_comm], exact nat.lt_succ_self _ },
  cases d₁; cases d₂; injection e with e1 e2; cases e2;
  try { cases e1 }; [refl, cases this e1.symm, cases this e1, refl]
end

theorem steps_tensor_unique_prev (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_tensor Ai Bi Ci X Z → steps_tensor Ai Bi Ci Y Z → X = Y :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_tensor_unique_next (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_tensor Ai Bi Ci X Y → steps_tensor Ai Bi Ci X Z → Y = Z :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_par_unique_prev (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_par Ai Bi Ci X Z → steps_par Ai Bi Ci Y Z → X = Y :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_par_unique_next (Ai Bi Ci : Form_occ) (X Y Z) : Ai ≠ Bi → Bi ≠ Ci → Ai ≠ Ci → steps_par Ai Bi Ci X Y → steps_par Ai Bi Ci X Z → Y = Z :=
begin
  intros _ _ _ s₁ s₂,
  cases s₁; cases s₂; try {refl}; try {contradiction},
end

theorem steps_unique_prev (T : switch) (Δ : Link) (hΔ : valid_link Δ) (X Y Z) : steps T Δ X Z → steps T Δ Y Z → X = Y :=
begin
  intros s₁ s₂,
  cases s₁,
  case steps.ax : A ai ni Bi Ci d₁ {
    cases s₂ with _ _ _ Di _ d₂,
    rw dual_unique_prev d₁ d₂ },
  case steps.cut : A ai ni Bi Ci d₁ {
    rcases s₂ with _ | ⟨_,_,_,Di,_,d₂⟩,
    rw dual_unique_prev d₂ d₁
  },
  case steps.con : A ai { cases s₂, refl },
  case steps.tensor : A B ai bi ci X y t₁ {
    rcases s₂ with _ | _ | _ | ⟨_,_,_,_,_,_,_,t₂⟩,
    cases T, apply steps_tensor_unique_prev _ _ _ _ _ _ _ _ _ t₁ t₂,
    cases hΔ, finish, rw flip_L,

  },
end

[Mario Carneiro]

oh, you have to rw flip_L at t₁ t₂

[Billy Price]

Shouldn't I be able to just simp?

[Mario Carneiro]

it still has to be at t₁ t₂

[Mario Carneiro]

otherwise it will only simplify the goal, which does not mention flip

[Mario Carneiro]

you can also at * but this is usually not a good idea

[Billy Price]

ah okay cheers

[Billy Price]

How can I prove the example here using the lemma, since I can't use cases on the e?

import tactic

inductive Form : Type
| atom : ℕ → Form
| tensor : Form → Form → Form
| par : Form → Form → Form
| neg : Form → Form

infix ` ⊗ `:70 := Form.tensor
infix ` ⅋ `:65 := Form.par
prefix `~` := Form.neg

lemma not_self_sub_left_tensor {A B} : A ≠ A ⊗ B :=
begin
  intro e,
  apply_fun Form.sizeof at e,
  refine ne_of_lt _ e,
  rw [Form.sizeof, nat.add_comm],
  apply nat.lt_of_succ_le,
  rw nat.add_comm, rw nat.add_comm 1,
  apply nat.le_add_right,
end

example {A B} {n m : ℕ} : (A,n) ≠ (A ⊗ B, m) :=
begin
  intro e,
end

[Mario Carneiro]

use injection

[Mario Carneiro]

injection e with e1, apply not_self_sub_left_tensor e1

[Billy Price]

I have some candidate definitions for a trip around a proof net, and I'd like to understand how the choices involved would affect the usability. The first definition I wrote was what is now called list_trip, but the downside was it doesn't explicate where the trip ends. That's important for my later definitions, because I will be constantly talking about partial trips that start with Ai↓ and end with Ai↑, and I also want to define cyclic trips, which start and end with the same thing. Those motivations inspired trip1 and trip2. trip1 seems to me like I'm defining my own list type with extra constraints, and trip2 is the same but I get to add to either end.

So what considerations should I take into account when choosing a definition here?

inductive trip1 (ps : proof_structure) (S : switching) : Form_occ × dir → Form_occ × dir → Prop
| single (Ai : Form_occ) (d : dir) : Ai ∈ ps → trip1 (Ai,d) (Ai,d)
| cons (Ai Bi Ci : Form_occ) (d₁ d₂ d₃ : dir) (Δ : Link) :
  Δ ∈ ps.links → steps (S Δ) Δ (Ai,d₁) (Bi,d₂) → trip1 (Bi,d₂) (Ci, d₃) → trip1 (Ai,d₁) (Ci,d₃)

inductive trip2 (ps : proof_structure) (S : switching) : Form_occ × dir → Form_occ × dir → Prop
| single (Ai : Form_occ) (d : dir) : Ai ∈ ps → trip2 (Ai,d) (Ai,d)
| front (Ai Bi Ci : Form_occ) (d₁ d₂ d₃ : dir) (Δ : Link) :
  Δ ∈ ps.links → steps (S Δ) Δ (Ai,d₁) (Bi,d₂) → trip2 (Bi,d₂) (Ci, d₃) → trip2 (Ai,d₁) (Ci,d₃)
| back (Ai Bi Ci : Form_occ) (d₁ d₂ d₃ : dir) (Δ : Link) :
  Δ ∈ ps.links → steps (S Δ) Δ (Bi,d₂) (Ci,d₃) → trip2 (Ai,d₁) (Bi, d₂) → trip2 (Ai,d₁) (Ci,d₃)

inductive list_trip (ps : proof_structure) (S : switching) : list (Form_occ × dir) → Prop
| emp : list_trip []
| single (Ai : Form_occ) (d : dir) : Ai ∈ ps → list_trip [(Ai,d)]
| cons (Ai Bi : Form_occ) (d₁ d₂ : dir) (Γ : list (Form_occ × dir)) (Δ : Link) :
  Δ ∈ ps.links → steps (S Δ) Δ (Ai,d₁) (Bi,d₂) → list_trip ((Bi,d₂) :: Γ) → list_trip ((Ai,d₁) :: (Bi,d₂) :: Γ)

[Billy Price]

I've pushed ahead with the trip1 definition but I also added a trip length (nat) parameter. Is that a bad idea?

inductive trip (ps : proof_structure) (S : switching) : ℕ → Form_occ × dir → Form_occ × dir → Prop
| single {Ai d}    : Ai ∈ ps → trip 0 (Ai,d) (Ai,d)
| cons {X Y Z Δ n} : Δ ∈ ps.links → steps (S Δ) Δ X Y → trip n Y Z → trip (n.succ) X Z

I went on to define trip.rcons as dual to trip.cons, where I can extend a trip on the other end with def trip.rcons {Δ} : Δ ∈ ps.links → trip ps S n X Y → steps (S Δ) Δ Y Z → trip ps S n.succ X Z.

Having trip.cons as a constructor for trip was very useful to prove this theorem
trip ps S n X Z → trip ps S n Y Z → X = Y
I did it by induction on n and then I broke down the two trips with into their trip.cons constructions.

I'm now trying to prove this theorem trip_unique_stop : trip ps S n X Y → trip ps S n X Z → Y = Z, for which I'd like to do the same thing (induction on n), but then in the nat.succ case I need to break down the two trips not into their trip.cons components, but into their canonical trip.rcons components.

I tried to generalise this into a lemma trip_rcons_decompose {α : Prop} (f : Π Δ Y, Δ ∈ ps.links → trip ps S n X Y → steps (S Δ) Δ Y Z → α) : trip ps S n.succ X Z → α, but I've essentially moved the problem. What can I do?

[Billy Price]

hmm, seems my mwe is too big for one message. Here's the file. Lemme know if I should provide it another way. mll.lean

[Billy Price]

Okay I went ahead and made a better mwe with sorry's, enjoy :)

import tactic

inductive Form : Type
| atom : ℕ → Form
| tensor : Form → Form → Form
| par : Form → Form → Form
| neg : Form → Form

infix ` ⊗ `:70 := Form.tensor
infix ` ⅋ `:65 := Form.par
prefix `~` := Form.neg

inductive Link : Type
| ax : ℕ → ℕ → Form → Link
| cut : ℕ → ℕ → Form → Link
| tensor : ℕ → ℕ → ℕ → Form → Form → Link
| par : ℕ → ℕ → ℕ → Form → Form → Link
| con : ℕ → Form → Link

def Form_occ := Form × ℕ

inductive premise : Form_occ → Link → Prop
| cut_pos {A i j}          : premise (A,i) (Link.cut i j A)
| cut_neg {A i j}          : premise (~A,j) (Link.cut i j A)
| tensor_left {A B i j k}  : premise (A,i) (Link.tensor i j k A B)
| tensor_right {A B i j k} : premise (B,j) (Link.tensor i j k A B)
| par_left {A B i j k}     : premise (A,i) (Link.par i j k A B)
| par_right {A B i j k}    : premise (B,j) (Link.par i j k A B)
| con {A i}                : premise (A,i) (Link.con i A)

inductive conclusion : Form_occ → Link → Prop
| ax_pos {A i j}     : conclusion (A,i) (Link.ax i j A)
| ax_neg {A i j}     : conclusion (~A,j) (Link.ax i j A)
| tensor {A B i j k} : conclusion (A ⊗ B,k) (Link.tensor i j k A B)
| par {A B i j k}    : conclusion (A ⅋ B,k) (Link.par i j k A B)

inductive valid_link : Link → Prop
| ax  (i j A) : valid_link (Link.ax i j A)
| cut (i j A) : valid_link (Link.cut i j A)
| con (i A) : valid_link (Link.con i A)
| tensor (i j k A B) : (A,i) ≠ (B,j) → valid_link (Link.tensor i j k A B)
| par (i j k A B) : (A,i) ≠ (B,j) → valid_link (Link.par i j k A B)

structure proof_structure : Type :=
(links : set Link)
(valid : ∀ l ∈ links, valid_link l)
(prem_unique : ∀ Ai : Form_occ, ∀ l₁ l₂ ∈ links, premise Ai l₁ → premise Ai l₂ → l₁ = l₂)
(con_unique : ∀ Ai : Form_occ, ∀ l₁ l₂ ∈ links, conclusion Ai l₁ → conclusion Ai l₂ → l₁ = l₂)

inductive mem_Form_occ_ps (Ai : Form_occ) (ps : proof_structure) : Prop
| prem (l) : l ∈ ps.links → premise Ai l → mem_Form_occ_ps
| con (l) : l ∈ ps.links → conclusion Ai l → mem_Form_occ_ps

instance : has_mem Form_occ proof_structure := ⟨mem_Form_occ_ps⟩

@[reducible]
def dir := bool

@[pattern] def down := ff
@[pattern] def up := tt

@[pattern] def with_down (Ai : Form_occ) := (Ai,down)
@[pattern] def with_up (Ai : Form_occ) := (Ai,up)
postfix `↓`:max_plus := with_down
postfix `↑`:max_plus := with_up

@[reducible]
def switch := bool

@[reducible, pattern] def L := ff
@[reducible, pattern] def R := tt

def switching := Link → switch

@[simp]
def switch.flip {α β} (f : α → α → β) : switch → α → α → β
| L a b := f a b
| R a b := f b a

inductive steps_tensor (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_tensor Ai↓ Ci↓
| turn : steps_tensor Bi↓ Ai↑
| up : steps_tensor Ci↑ Bi↑

inductive steps_par (Ai Bi Ci : Form_occ) : Form_occ × dir → Form_occ × dir → Prop
| down : steps_par Ai↓ Ci↓
| turn : steps_par Bi↓ Bi↑
| up : steps_par Ci↑ Ai↑

inductive dual (A : Form) (ai ni : ℕ) : Form_occ → Form_occ → Prop
| posneg : dual (A,ai) (~A,ni)
| negpos : dual (~A,ni) (A,ai)

inductive steps (T : switch) : Link → Form_occ × dir → Form_occ × dir → Prop
| ax  {A ai ni Bi Ci} : dual A ai ni Bi Ci → steps (Link.ax ai ni A) Bi↑ Ci↓
| cut {A ai ni Bi Ci} : dual A ai ni Bi Ci → steps (Link.cut ai ni A) Bi↓ Ci↑
| con {A ai}          : steps (Link.con ai A) (A, ai)↓ (A,ai)↑
| tensor {A B ai bi ci X Y} :
  T.flip steps_tensor (A, ai) (B, bi) (A ⊗ B, ci) X Y →
  steps (Link.tensor ai bi ci A B) X Y
| par {A B ai bi ci X Y} :
  T.flip steps_par (A, ai) (B, bi) (A ⅋ B, ci) X Y →
  steps (Link.par ai bi ci A B) X Y

inductive trip (ps : proof_structure) (S : switching) : ℕ → Form_occ × dir → Form_occ × dir → Prop
| single {Ai d}    : Ai ∈ ps → trip 0 (Ai,d) (Ai,d)
| cons {X Y Z Δ n} : Δ ∈ ps.links → steps (S Δ) Δ X Y → trip n Y Z → trip (n.succ) X Z

section
  variable {Δ : Link}
  variable {T : switch}
  variables {Ai Bi Ci : Form_occ}
  variables {X Y Z : Form_occ × dir}

  theorem steps_unique_prev : valid_link Δ → steps T Δ X Z → steps T Δ Y Z → X = Y := sorry

  theorem steps_unique_next : valid_link Δ → steps T Δ X Y → steps T Δ X Z → Y = Z := sorry

  lemma mem_ps_of_steps_next {ps : proof_structure} {d : dir} :
    Δ ∈ ps.links → steps T Δ X (Bi,d) → Bi ∈ ps := sorry

end

section
  variable {ps : proof_structure}
  variable {S : switching}
  variables {X Y Z : Form_occ × dir}
  variables {n m : ℕ}

  theorem link_unique_of_steps_prev {Δ₁ Δ₂} :
    Δ₁ ∈ ps.links → Δ₂ ∈ ps.links → steps (S Δ₁) Δ₁ X Y → steps (S Δ₂) Δ₂ X Z → Δ₁ = Δ₂ := sorry

  theorem link_unique_of_steps_next {Δ₁ Δ₂} :
    Δ₁ ∈ ps.links → Δ₂ ∈ ps.links → steps (S Δ₁) Δ₁ X Z → steps (S Δ₂) Δ₂ Y Z → Δ₁ = Δ₂ := sorry

  def trip.rcons {Δ} : Δ ∈ ps.links → trip ps S n X Y → steps (S Δ) Δ Y Z → trip ps S n.succ X Z :=
  begin
    revert X Y Z,
    induction n,
    case nat.zero : {
      rintros X Y Z hΔ ⟨Ai,d,hA⟩ s,
      apply trip.cons hΔ s,
      cases Z with Ci d',
      apply trip.single,
      apply mem_ps_of_steps_next hΔ s,
    },
    case nat.succ : n ih {
      rintros X Y Z hΔ tXY sYZ,
      cases tXY with _ _ _ _ W _ Δ' _ hΔ' sXW tWY,
      apply trip.cons hΔ' sXW,
      apply ih hΔ tWY sYZ,
    },
  end

  theorem trip_unique_start : trip ps S n X Z → trip ps S n Y Z → X = Y :=
  begin
    intros tX tY,
    revert X Y,
    induction n,
    case nat.zero : { intros, cases tX; cases tY, refl},
    case nat.succ : n ih {
      rintros X Y tX tY,
      rcases tX with _ | ⟨_,X',_,Δ,_,hΔ,sX,tX'⟩,
      rcases tY with _ | ⟨_,Y',_,Δ',_,hΔ',sY,tY'⟩,
      have : Y' = X', by exact ih tY' tX',
      rw this at sY,
      have : Δ' = Δ, apply link_unique_of_steps_next hΔ' hΔ sY sX,
      rw this at sY,
      exact steps_unique_prev (ps.valid Δ hΔ) sX sY,
      }
  end

  lemma trip_rcons_decompose {α : Prop} (f : Π Δ Y, Δ ∈ ps.links → trip ps S n X Y → steps (S Δ) Δ Y Z → α) :
    trip ps S n.succ X Z → α :=
  begin
    sorry
  end

  theorem trip_unique_stop : trip ps S n X Y → trip ps S n X Z → Y = Z :=
  begin
    revert Y Z,
    induction n,
    case nat.zero : { intros _ _ tXY tXZ, cases tXY, cases tXZ, refl},
    case nat.succ : n ih {
      rintros Y Z tXY tXZ,
      apply trip_rcons_decompose _ tXY,
      intros Δ V hΔ tXV sVY,
      apply trip_rcons_decompose _ tXZ,
      intros Δ' W hΔ' tXW sWZ,
      have : W = V, apply ih tXW tXV,
      rw this at sWZ,
      have : Δ' = Δ, apply link_unique_of_steps_prev hΔ' hΔ sWZ sVY,
      rw this at sWZ,
      apply steps_unique_next (ps.valid Δ hΔ) sVY sWZ,
      }
  end

end

[Billy Price]

Yay I managed to prove lemma trip_exists_rcons : trip ps S n.succ X Z → ∃ Y Δ, ∃ hΔ : Δ ∈ ps.links, ∃ tXY : trip ps S n X Y, steps (S Δ) Δ Y Z by induction on n. My question remain about

1. The consequences of choosing between trip1, trip2 and list_trip
2. Pros and cons of including a length parameter in the trip definition

[Billy Price]

I'm in a pickle, my aim is to define a map proof Γ -> proof_structure, but the definition of that map requires inductive reasoning on the properties of already constructed proof_structures. That property could be stated "every formula in Γ is available in the proof structure", where available means it's in some link but it's not a premise of any link. I tried to strengthen the concept of a proof_structure to the inductive type proof_net : sequent -> Type

inductive proof_net : sequent → Type
| mk {Γ : sequent} (ps : proof_structure) : (∀ A ∈ Γ, ∃ i, ∃ Δ ∈ ps.links, conclusion (A,i) Δ ∧ ∀ Δ' ∈ ps.links, ¬premise (A,i) Δ') → proof_net Γ

but I need to utilise the existential i's and Δ's to define the map proof Γ -> proof_net Γ, which is impossible since I'm not eliminating into Prop.

What can I do? I'm not married to this definition proof_net Γ at all, it's just my latest attempt to define something that assists me in defining proof Γ -> proof_structure.

[Billy Price]

here's my mwe with a failed attempt to define the tensor map case at the bottom

import tactic

inductive Form : Type
| atom : ℕ → Form
| tensor : Form → Form → Form
| par : Form → Form → Form
| neg : Form → Form

infix ` ⊗ `:70 := Form.tensor
infix ` ⅋ `:65 := Form.par
prefix `~` := Form.neg

inductive Link : Type
| ax : ℕ → ℕ → Form → Link
| cut : ℕ → ℕ → Form → Link
| tensor : ℕ → ℕ → ℕ → Form → Form → Link
| par : ℕ → ℕ → ℕ → Form → Form → Link

def Form_occ := Form × ℕ

inductive premise : Form_occ → Link → Prop
| cut_pos {A i j}          : premise (A,i) (Link.cut i j A)
| cut_neg {A i j}          : premise (~A,j) (Link.cut i j A)
| tensor_left {A B i j k}  : premise (A,i) (Link.tensor i j k A B)
| tensor_right {A B i j k} : premise (B,j) (Link.tensor i j k A B)
| par_left {A B i j k}     : premise (A,i) (Link.par i j k A B)
| par_right {A B i j k}    : premise (B,j) (Link.par i j k A B)

inductive conclusion : Form_occ → Link → Prop
| ax_pos {A i j}     : conclusion (A,i) (Link.ax i j A)
| ax_neg {A i j}     : conclusion (~A,j) (Link.ax i j A)
| tensor {A B i j k} : conclusion (A ⊗ B,k) (Link.tensor i j k A B)
| par {A B i j k}    : conclusion (A ⅋ B,k) (Link.par i j k A B)

inductive mem_Link (Ai : Form_occ) (l : Link) : Prop
| prem : premise Ai l → mem_Link
| con : conclusion Ai l → mem_Link

instance : has_mem Form_occ Link := ⟨mem_Link⟩

inductive valid_link : Link → Prop
| ax  {i j A} : valid_link (Link.ax i j A)
| cut {i j A} : valid_link (Link.cut i j A)
| tensor {i j k A B} : (A,i) ≠ (B,j) → valid_link (Link.tensor i j k A B)
| par {i j k A B} : (A,i) ≠ (B,j) → valid_link (Link.par i j k A B)

structure proof_structure : Type :=
(links : set Link)
(valid : ∀ l ∈ links, valid_link l)
(prem_unique : ∀ Ai : Form_occ, ∀ l₁ l₂ ∈ links, premise Ai l₁ → premise Ai l₂ → l₁ = l₂)
(con_unique : ∀ Ai : Form_occ, ∀ l₁ l₂ ∈ links, conclusion Ai l₁ → conclusion Ai l₂ → l₁ = l₂)

inductive mem_Form_occ_ps (Ai : Form_occ) (ps : proof_structure) : Prop
| mk {l} : l ∈ ps.links → Ai ∈ l → mem_Form_occ_ps

instance : has_mem Form_occ proof_structure := ⟨mem_Form_occ_ps⟩

def sequent := list Form

instance : has_append sequent := ⟨list.append⟩
instance : has_mem Form sequent := ⟨list.mem⟩

inductive proof : sequent → Type
| ax (A)                   : proof [~A, A]
| cut (A) {Γ Γ' Δ Δ'}      : proof (Γ ++ [A] ++ Γ') → proof (Δ ++ [~A] ++ Δ') → proof (Γ++Γ'++Δ++Δ')
| tensor {A B} {Γ Γ' Δ Δ'} : proof (Γ ++ [A] ++ Γ') → proof (Δ ++ [B] ++ Δ') → proof (Γ++Γ'++ [A ⊗ B] ++Δ++Δ')
| par {A B} {Γ Γ'}         : proof (Γ ++ [A,B] ++ Γ') → proof (Γ ++ [A ⅋ B] ++ Γ')
| ex {A B} {Γ Γ'}          : proof (Γ ++ [A,B] ++ Γ') → proof (Γ ++ [B,A] ++ Γ')

inductive proof_net : sequent → Type
| mk {Γ : sequent} (ps : proof_structure) : (∀ A ∈ Γ, ∃ i, ∃ Δ ∈ ps.links, conclusion (A,i) Δ ∧ ∀ Δ' ∈ ps.links, ¬premise (A,i) Δ') → proof_net Γ

instance {Γ : sequent} : has_coe (proof_net Γ) proof_structure := ⟨by rintro ⟨Γ,ps,_⟩; exact ps⟩

def relabel_Link (f : ℕ → ℕ) : Link → Link
| (Link.ax pi ni A) := Link.ax (f pi) (f ni) A
| (Link.cut pi ni A) := Link.cut (f pi) (f ni) A
| (Link.tensor ai bi ci A B) := Link.tensor (f ai) (f bi) (f ci) A B
| (Link.par ai bi ci A B) := Link.par (f ai) (f bi) (f ci) A B

def proof_structure.relabel (ps : proof_structure) (f : ℕ → ℕ) (hf : function.injective f) : proof_structure :=
⟨set.image (relabel_Link f) ps.links, sorry, sorry, sorry⟩

def separators {α β} (f g : α → β) : Prop := ∀ x y, f x ≠ g y

lemma sep_even_odd : separators (λ x, 2 * x) (λ x, 2 * x + 1) :=
  λ x y, nat.two_mul_ne_two_mul_add_one

def disjoint_of_separators {ps₁ ps₂ : proof_structure} {f g} (hf hg) : separators f g → disjoint { Ai | Ai ∈ (ps₁.relabel f hf) } { Ai | Ai ∈ (ps₂.relabel g hg) } :=
 by sorry

def proof_net.disjoint {Γ Δ} : proof_net Γ → proof_net Δ → Prop :=
  by rintro ⟨_,ps₁,_⟩ ⟨_,ps₂,_⟩; exact disjoint {Ai | Ai ∈ ps₁} {Ai | Ai ∈ ps₂}

def net_links_ax (pi ni A) : set Link :=
  {Link.ax pi ni A}

def net_links_tensor (ai bi ci A B) (sA sB : set Link) : set Link :=
  {Link.tensor ai bi ci A B} ∪ sA ∪ sB

def net_links_par (ai bi ci A B) (s : set Link) : set Link :=
  {Link.par ai bi ci A B} ∪ s

def net_links_cut (pi ni A) (sA snA : set Link) : set Link :=
  {Link.cut pi ni A} ∪ sA ∪ snA

def proof_net_ax (A) : proof_net [~A,A] :=
⟨
  ⟨{Link.ax 0 0 A},
  by rintro l ⟨h⟩; exact valid_link.ax,
  by rintro Ai Δ₁ Δ₂ ⟨_⟩ ⟨_⟩; finish,
  by rintro Ai Δ₁ Δ₂ ⟨_⟩ ⟨_⟩; finish ⟩
,
  begin
    rintro B ⟨⟨_⟩⟩,
      refine ⟨0,Link.ax 0 0 A,by simp,conclusion.ax_neg,_⟩, rintro Δ' ⟨_⟩ ⟨_⟩,
    rcases H with ⟨⟨_⟩⟩,
      refine ⟨0,Link.ax 0 0 A,by simp,conclusion.ax_pos,_⟩, rintro Δ' ⟨_⟩ ⟨_⟩,
    cases H,
  end
⟩

def proof_net_tensor {Γ Γ' A B Δ Δ'} (pnA : proof_net (Γ ++ [A] ++ Γ')) (pnB : proof_net (Δ ++ [B] ++ Δ')) :
  pnA.disjoint pnB → proof_net (Γ ++ Γ' ++ [A ⊗ B] ++ Δ ++ Δ') :=
begin
  rcases pnA with ⟨_,psA, hA⟩,
  rcases pnB with ⟨_,psB, hB⟩,
  intro dAB,
  specialize hA A (by exact list.mem_append_left _ (list.mem_append_right _ (list.mem_cons_self A list.nil))),
  specialize hB B (by exact list.mem_append_left _ (list.mem_append_right _ (list.mem_cons_self B list.nil))),
  cases hA with ai ΔA hA,

end

[Horatiu Cheval]

Do you care about computability? If not, you could get the i and the \Delta noncomputably using choice.

[Horatiu Cheval]

If that's not good, maybe you could work with subsets or Sigma-types instead of exists?

inductive proof_net : sequent → Type
| mk {Γ : sequent} (ps : proof_structure) :
  (Π A ∈ Γ, {iΔ : (ℕ × Link) // iΔ.2 ∈ ps.links ∧ conclusion (A,iΔ.1) iΔ.2 ∧
   ∀ Δ' ∈ ps.links, ¬premise (A,iΔ.1) Δ'}) → proof_net Γ

and then

rcases hA with ⟨⟨i, Δ⟩, hA⟩,

will work in your last proof.

[Horatiu Cheval]

This change might require changes also in other areas of your code though

[Billy Price]

I think I care about computability simply because it would be absurd to think of it as not computable. Everything involved in the construction of the proof structure is finite. This is just a construction of a finite set of Links. I just want to be able to produce a set of links inductively that has the property of forming a proof structure, since all the constructions along the way are proof structures with the right formulas available to be linked.

[Billy Price]

Maybe I can define proof_net Γ -> set Link and then lift it to proof_structure after the fact

[Billy Price]

That being said, what is this? {iΔ : (ℕ × Link) //

[Billy Price]

the //

[Alex J. Best]

Its is the notation for docs#subtype.

[Horatiu Cheval]

Yes, sorry, I meant to say subtype, not subset in my answer. {x : a // p x} is the subtype of those x satisfying p which is very similar to ∃ x : a, p x, except this is a Type and not a Prop, so you can (computably) eliminate it into any sort.

[Billy Price]

Alright, now i'm running into the problem that I can't eliminate B ∈ [~A,A] into that subtype.

[Billy Price]

I mean in this instance I can get away with not eliminating it because the i is the same for both formulas, but in general that's a little annoying

[Billy Price]

Okay I just realised that the same formula A could appear in the sequent Γ multiple times, and if so there will be multiple distinct i such that (A,i) appears in some link in the proof structure. This is a little annoying. A further detail that I think is implicit in the thing I'm trying to formalise, is that the i chosen for each A in the sequent should be the exact one that corresponds to the introduction of that A in the construction of the sequent.

[Horatiu Cheval]

Alright, now i'm running into the problem that I can't eliminate B ∈ [~A,A] into that subtype.

If you mean that you can't get that B is either ~A or A by casing on the list membership, that's true, but I'm sure it's possible to obtain that and write your definition in terms of those cases without needing to eliminate a Prop (like with an if then else or by_cases or something)

[Horatiu Cheval]

Sorry, I don't think I can give opinions on the larger design because I don't really understand what you're doing, I'm not familiar with these things :) I was just trying to help with the more specific Lean-related technical problems

[Billy Price]

That's okay, could you explain how I would change things here to use if then else or by_cases?

def proof_net_ax (A) : proof_net [~A,A] :=
⟨
  ⟨{Link.ax 0 0 A},
  by rintro l ⟨h⟩; exact valid_link.ax,
  by rintro Ai Δ₁ Δ₂ ⟨_⟩ ⟨_⟩; finish,
  by rintro Ai Δ₁ Δ₂ ⟨_⟩ ⟨_⟩; finish ⟩
,
  begin
    rintro B Bmem,
    cases Bmem,
      exact ⟨0,Link.ax 0 0 A,by simp,conclusion.ax_neg,_⟩, rintro Δ' ⟨_⟩ ⟨_⟩,
    rcases H with ⟨⟨_⟩⟩,
      exact ⟨0,Link.ax 0 0 A,by simp,conclusion.ax_pos,_⟩, rintro Δ' ⟨_⟩ ⟨_⟩,
    cases H,
  end
⟩

[Billy Price]

actually the stuff after cases Bmem is outdated, but i can't "go in and fix it" until i get past cases Bmem

[Billy Price]

I suppose, as I mentioned before, it doesn't matter here because i is 0 in both. hmm

[Horatiu Cheval]

This shouls work if I understand correctly what you need here

def proof_net_ax (A) : proof_net [~A,A] :=
⟨
  ⟨{Link.ax 0 0 A},
  by rintro l ⟨h⟩; exact valid_link.ax,
  by rintro Ai Δ₁ Δ₂ ⟨_⟩ ⟨_⟩; finish,
  by rintro Ai Δ₁ Δ₂ ⟨_⟩ ⟨_⟩; finish ⟩
,
  begin
    rintro B _,
    simp at H,
    by_cases hBA : B = A,
    {
      -- hre you have
      -- hBA : B = A
      sorry,
    },
    {
      have : B = ~A := by {
        cases H,
        { assumption },
        { contradiction, }
      },
      sorry,
      -- here you have
      -- this : B = ~A
    },
  end
⟩

[Horatiu Cheval]

It's quite ugly I think, I'm sure it could be done more elegantly, but just as an example

[Jannis Limperg]

Billy Price said:

Okay I just realised that the same formula A could appear in the sequent Γ multiple times, and if so there will be multiple distinct i such that (A,i) appears in some link in the proof structure. This is a little annoying. A further detail that I think is implicit in the thing I'm trying to formalise, is that the i chosen for each A in the sequent should be the exact one that corresponds to the introduction of that A in the construction of the sequent.

It's very common for informal texts to gloss over stuff like this. The carefully written ones at least have a sentence somewhere saying, "actually our contexts are multisets but we're not going to talk about it". If so, you need to either adjust your context definition or make sure that your other definitions can deal with reordering and/or duplicates.

[Billy Price]

I'm using ∈ but my sequent's are in fact lists, not sets. I think this stems from a purism about what sequents are, but for my purpose the identity of a sequent is less important than the idea that a proof/derivation of a sequent corresponds precisely to a construction of a proof net, and that construction is blind to exchange rules.

[Billy Price]

The moral being I don't think the sequent, as a list or multiset, has enough information to identify a canonical occurrence in a proof structure for each formula in the sequent, because any derivation can just finish with a bunch of exchange rules. It's really the whole proof structure you need to identify which formula corresponds to which.

[Billy Price]

I guess the reason a sequent is a list is really because a point of the proof net is to identify distinct proofs that differ only by exchange rules.

[Billy Price]

that being said, I don't even believe that now, because a use of exchange on identical formulas before a logical rule can change how you should construct the proof net. For example if you tensor two proofs with sequents [A] and [B,B] to get [A \ox B, B], the construction of the proof net is different if you exchange the B's first.

[Yakov Pechersky]

Use docs#list.nth_le_of_mem. Then you have a finite number of specified indices to check.