Using previously provided data when proving instances

Stream: new members

[Abdullah Uyu]

I have this class:

class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  l1  : ∀ a b , ell a b a
  l2  : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q, ell q a c ∧ ell q b d

And I am proving that an object I constructed is an instance of this class. I proved l1 and l2, and when proving l3, I need l1 and l2. Can I access the proofs of them? What are the names?

⟨
by
-- proof of l1
done,

by
-- proof of l2
done,

by
-- I want to access the proof of l1 and l2 here!
done
⟩

[Abdullah Uyu]

Maybe I should note, the code itself is not actually important. I just wanted to explain the form of the context.

[Abdullah Uyu]

Alright, removed the unessential parts.

[Eric Wieser]

Can you make this a #mwe? You second code block is missing the instance keyword etc needed to make it valid.

[Abdullah Uyu]

It got a bit longer but I did my best to shorten it. I also annotated the parts I am interested in.

import Mathlib.Tactic

open Set

variable [DecidableEq G]

namespace Subspace

class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  l1  : ∀ a b , ell a b a
  l2  : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q, ell q a c ∧ ell q b d

def star
  [ProjectiveGeometry G ell]
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}

class Subspace
  (PG : ProjectiveGeometry G ell) where
  E : Set G
  closure : ∀ a b, a ∈ E → b ∈ E → star (ell := ell) a b ⊆ E

class ProjectiveSubgeometry
  (PG : ProjectiveGeometry G ell)
  (G' : Set G) where
  ell' : G' → G' → G' → Prop
  restriction : ∀ a b c : G', ell' a b c = ell a b c
  inst : ProjectiveGeometry G' ell'

theorem l1_l2_eq_imp_l3
  (ell : G → G → G → Prop)
  (a b c d p : G)
  (l1 : ∀ a b , ell a b a)
  (l2 : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p)
  (abcdp_deq : a = b ∨ a = c ∨ a = d ∨ a = p ∨ b = c ∨ b = d ∨ b = p
               ∨ c = d ∨ c = p ∨ d = p)
  (pab_col : ell p a b)
  (pcd_col : ell p c d) :
    ∃ q, ell q a c ∧ ell q b d := by
  sorry

instance
  [PG : ProjectiveGeometry G ell]
  [S : Subspace PG] :
    ProjectiveSubgeometry PG S.E :=
  ⟨
  fun a b c => S.E.restrict (S.E.restrict (S.E.restrict ell a) b) c,

  by
  intro a b c
  simp
  done,

  ⟨
  by -- I prove l1 here.
  simp only [restrict]
  intro a b
  apply PG.l1 a b
  done,

  by -- I prove l2 here.
  simp only [restrict]
  intro a b p q apq_col bpq_col pq_neq
  apply PG.l2 a b p q apq_col bpq_col
  intro ppqq_eq
  have pq_eq : p = q := by { exact SetCoe.ext ppqq_eq }
  contradiction
  done,

  by
  simp only [restrict]
  intro a b c d p pab_col pcd_col
  have q_ex :
      ∃ q, ell q a c ∧ ell q b d := by
    apply PG.l3 a b c d p pab_col pcd_col
  by_cases deq : (a = b ∨ a = c ∨ a = d ∨ a = p ∨ b = c ∨ b = d ∨ b = p
                ∨ c = d ∨ c = p ∨ d = p)
  · let ell' := fun a b c => S.E.restrict
                            (S.E.restrict
                            (S.E.restrict ell a) b) c
    apply l1_l2_eq_imp_l3 ell' a b c d p _ _ deq pab_col pcd_col
    · sorry -- Here I need l1 I proved above.
    · sorry -- Here I need l2 I proved above.
  · sorry -- This sorry is irrelevant.
  done
  ⟩
  ⟩

end Subspace

[Ted Hwa]

I proved l1 and l2, and when proving l3, I need l1 and l2. Can I access the proofs of them? What are the names?

You have give names to the proofs using have. For example:

have proof_of_l1 := by
   ...

have proof_of_l2 := by
   ...

have proof_of_l3 := by
  ...
  -- here you can use proof_of_l1 and proof_of_l2

[Abdullah Uyu]

I am having a bit of trouble understanding the context of your suggestion. Do I write these between "⟨" and "⟩"? For example when I try to convert my proof of l1 to a have statement, I get:

...
  ⟨
  have proof_of_l1 := by
    simp only [restrict]
    intro a b
    apply PG.l1 a b
    done
...

invalid constructor ⟨...⟩, insufficient number of arguments, constructs 'Basic.ProjectiveGeometry.mk' has #3 explicit fields, but only #2 provided

So I get that the block is no longer recognized as a constructor. Meanwhile I read that I can say where and explicitly provide data, but in that case I couldn't figure out how can I write the inner instance explicitly.

I was going to try to access ell' anyways, and I tried that, but that gives unknown identifier 'ell'', so the outer instance's constructors are not passed to the scope of the inner one? I hope I make sense, I sensed that my goal didn't get to you because maybe I couldn't provide a simpler example. Here is my try:

import Mathlib.Tactic

open Set

variable [DecidableEq G]

namespace Structures

class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  l1  : ∀ a b , ell a b a
  l2  : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q, ell q a c ∧ ell q b d

def star
  [ProjectiveGeometry G ell]
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}

class Subspace
  (PG : ProjectiveGeometry G ell) where
  E : Set G
  closure : ∀ a b, a ∈ E → b ∈ E → star (ell := ell) a b ⊆ E

class ProjectiveSubgeometry
  (PG : ProjectiveGeometry G ell)
  (G' : Set G) where
  ell' : G' → G' → G' → Prop
  restriction : ∀ a b c : G', ell' a b c = ell a b c
  inst : ProjectiveGeometry G' ell'

theorem l1_l2_eq_imp_l3
  (ell : G → G → G → Prop)
  (a b c d p : G)
  (l1 : ∀ a b , ell a b a)
  (l2 : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p)
  (abcdp_deq : a = b ∨ a = c ∨ a = d ∨ a = p ∨ b = c ∨ b = d ∨ b = p
               ∨ c = d ∨ c = p ∨ d = p)
  (pab_col : ell p a b)
  (pcd_col : ell p c d) :
    ∃ q, ell q a c ∧ ell q b d := by
  sorry

instance
  [PG : ProjectiveGeometry G ell]
  [S : Subspace PG] :
    ProjectiveSubgeometry PG S.E where
  ell' := fun a b c => S.E.restrict (S.E.restrict (S.E.restrict ell a) b) c

  -- restriction is trivial.
  restriction := by
    intro a b c
    simp
    done

  inst := ⟨
  by
  simp only [restrict]
  intro a b
  apply PG.l1 a b
  done,

  by
  simp only [restrict]
  intro a b p q apq_col bpq_col pq_neq
  apply PG.l2 a b p q apq_col bpq_col
  intro ppqq_eq
  have pq_eq : p = q := by { exact SetCoe.ext ppqq_eq }
  contradiction
  done,

  by
  simp only [restrict]
  intro a b c d p pab_col pcd_col
  have q_ex :
      ∃ q, ell q a c ∧ ell q b d := by
    { apply PG.l3 a b c d p pab_col pcd_col }
  by_cases deq : (a = b ∨ a = c ∨ a = d ∨ a = p ∨ b = c ∨ b = d ∨ b = p
                ∨ c = d ∨ c = p ∨ d = p)
  · -- let ell' := fun a b c => S.E.restrict
    --                         (S.E.restrict
    --                         (S.E.restrict ell a) b) c
    apply l1_l2_eq_imp_l3 ell' a b c d p _ _ deq pab_col pcd_col
    · sorry
    · sorry
  · sorry
  done
  ⟩

end Structures

[Abdullah Uyu]

See that out of desperation, I was redefining ell' by copy pasting. To try to access the previous constructor now I explicitly have, I commented that redefinition in my recent try. It's not in the scope.

[Abdullah Uyu]

@Ted Hwa Am I missing something here? Is this not possible or maybe not reasonable to have as a feature?

[Abdullah Uyu]

I mean, do I have to prove these properties l1 and l2 outside of the instance construction?

[Yaël Dillies]

Your issues might be symptomatic of the fact that you are missing a custom constructor for ProjectiveGeometry

[Abdullah Uyu]

Oh shoot, I am importing Basic above, it's my own file. I am so sorry. Let me fix that so it runs.

[Abdullah Uyu]

Alright, now it errors as I explained. Sorry again, I thought I checked then.

[Abdullah Uyu]

@Yaël Dillies I don't think I understand what you mean. The ProjectiveGeometry class was not in the code above, I missed it because of my import. How does it look now?

[Yaël Dillies]

Ah, I partly based myself off your original message

[Abdullah Uyu]

I see, no problem. I think my problem is now best visible in the most recent snippet above.

[Yaël Dillies]

What I am saying is that you might be able to define a function def ProjectiveGeometry.ofSomething ... : ProjectiveGeometry G ell which takes care for you of feeding l1 and l2 into l3

[Abdullah Uyu]

I guess I got it. Alright, I will try that.

[Yaël Dillies]

The hope of course is that ProjectiveGeometry.ofSomething has a nice mathematical interpretation. I can't guarantee this will be the case