Dumping derivations of inductive predicate

Stream: Is there code for X?

[Thomas Vigouroux]

So I have an inductive predicate Finset A -> A -> Prop, and I'd like to "dump" the derivation to a string, so that I can make simple programs computing such derivations and then outputting them.

Is there a simple way to do that ?

[Eric Wieser]

Can you give a mwe that indicates the behavior you want?

[Thomas Vigouroux]

I'll write something but basically take GlimpseOfLean, in the file intuitionistic propositional logic, I'd like to dump a specific derivation of ProvableFrom

[Eric Wieser]

It's very helpful if you can write a self-contained example on Zulip itself, even if you just copy-paste from GlimpseOfLean

[Thomas Vigouroux]

Yeah I'll write that in a sec, I'm afk for a few minutes

[Thomas Vigouroux]

Here it is:

import Mathlib.Tactic
import Mathlib.Data.Finset.Basic

abbrev Variable := String

-- Formulas
inductive Formula
| bot
| var : Variable → Formula
| and : Formula → Formula → Formula
| or : Formula → Formula → Formula
| imp : Formula → Formula → Formula
deriving DecidableEq

instance : HAnd Formula Formula Formula where
  hAnd := Formula.and

instance : HOr Formula Formula Formula where
  hOr := Formula.or

notation:max (priority := high) "#" v:max => Formula.var v
infixr:27 (priority := high) " ⟹ " => Formula.imp

instance: Bot Formula where
  bot := Formula.bot

set_option hygiene false
infix:27 (priority:=high) " ⊢ " => Sequent

-- Derivations
inductive Sequent : Finset Formula → Formula → Prop
| Ax : #v ∈ Γ → Γ ⊢ #v
| ExFalso : ⊥ ∈ Γ → Γ ⊢ G
| AndI : Γ ⊢ A → Γ ⊢ B → Γ ⊢ A &&& B
| AndE : insert A (insert B Γ) ⊢ C → insert (A &&& B) Γ ⊢ C
| OrI1 : Γ ⊢ A → Γ ⊢ (A ||| B)
| OrI2 : Γ ⊢ B → Γ ⊢ (A ||| B)
| OrE : insert A Γ ⊢ C → insert B Γ ⊢ C → insert (A ||| B) Γ ⊢ C
| ImpI : insert A Γ ⊢ B → Γ ⊢ (A ⟹ B)
-- Now the ImpE rules, that are exploded by cases
-- Γ, a, B ⊢ C → Γ, a, a ⇒ B ⊢ C
| ImpEAtom : insert #v (insert B Γ) ⊢ C → insert #v (insert (#v ⟹ B) Γ) ⊢ C
| ImpEBot : Γ ⊢ C → insert (⊥ ⟹ B) Γ ⊢ C
| ImpEAnd : insert (A₁ ⟹ A₂ ⟹ B) Γ ⊢ C → insert ((A₁ &&& A₂) ⟹ B) Γ ⊢ C
| ImpEOr : insert (A₁ ⟹ B) (insert (A₂ ⟹ B) Γ) ⊢ C → insert ((A₁ ||| A₂) ⟹ B) Γ ⊢ C
| ImpEImp : insert A₁ (insert (A₂ ⟹ B) Γ) ⊢ A₂ → insert B Γ ⊢ C → insert ((A₁ ⟹ A₂) ⟹ B) Γ ⊢ C

def Sequent.dump (S: Γ ⊢ C): String := sorry

[Thomas Vigouroux]

And the point of interest being the function Sequent.dump

[Thomas Vigouroux]

Especially, this tentative implementation fails:

/-
tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Sequent.casesOn' can only eliminate into Prop
 after processing
  _, _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-/
def Sequent.dump (S: Γ ⊢ C): String := match S with
| Ax v => "Ax"
| _ => sorry

[Eric Wieser]

Right, you can't ask a Prop "how were you constructed" unless you promise you are only going to use that information to prove something

[Eric Wieser]

That's what

tactic 'induction' failed, recursor 'Sequent.casesOn' can only eliminate into Prop

means

[Thomas Vigouroux]

Then here goes my other question: what if I have Decidable (G |- C), then I can turn my Prop into a bool and use that ?

[Yaël Dillies]

Nonono, you're off by one level.

[Eric Wieser]

What's your end goal here: do you just want to see how a proof was built, or do you want to prove things about how the proof was built?

[Thomas Vigouroux]

Yaël Dillies said:

Nonono, you're off by one level.

Oh, because Bool: Type 1 right ?

[Eric Wieser]

If the former, you can just use #print some_sequent_proof and it will show you the construction

[Eric Wieser]

Which is fine because #print operates in the meta-theory on Expr objects

[Yaël Dillies]

Here's an example of what Eric is saying: If h : p ∨ q, you can't say "Oh I'll map h to 0 if it came from p and to 1 if it came from q" because it could come from both p and q!

[Yaël Dillies]

If you replace p ∨ q by p || q, you still get the same problem.

[Thomas Vigouroux]

My goal is to make a simple "prover" app for intuitionistic propositional logic, to which you give your context + goal, and it autoproves (if a proof exists)

[Thomas Vigouroux]

For that I thus need to output the resulting derivation

[Eric Wieser]

I don't think your conclusion necessarily follows there, it's quite possible that inspecting the Expr would work for you

[Eric Wieser]

Unless you want to prove the app itself is correct

[Thomas Vigouroux]

Eric Wieser said:

Unless you want to prove the app itself is correct

That I am fine doing be reasonning directly in the formalisation

[Thomas Vigouroux]

Eric Wieser said:

I don't think your conclusion necessarily follows there, it's quite possible that inspecting the Expr would work for you

How would I do that then ?

[Eric Wieser]

The other easy way out is to replace

inductive Sequent : Finset Formula → Formula → Prop

with

inductive Sequent : Finset Formula → Formula → Type

but that might make things unpleasant for you elsewhere

[Eric Wieser]

Thomas Vigouroux said:

How would I do that then ?

Can you add an example proof in your code so that I can demonstrate how to print it?

[Thomas Vigouroux]

Yup, because having that as a predicate helps for proving things like consistency and completeness

[Thomas Vigouroux]

Here's an example:

def v: Variable := "v"
def u: Variable := "u"

lemma Sequent.orComm: {#u ||| #v} ⊢ #v ||| #u := by {
  rw [← insert_emptyc_eq]
  apply OrE
  · apply OrI2
    apply Ax
    simp only [insert_emptyc_eq, Finset.mem_singleton]
  · apply OrI1
    apply Ax
    simp only [insert_emptyc_eq, Finset.mem_singleton]
}

[Thomas Vigouroux]

I'd really like to get the derivation printed out for Sequent.orComm in a way that I have control over

[Eric Wieser]

I guess

#print Sequent.orComm
-- theorem Sequent.orComm : Sequent {#u ||| #v} (#v ||| #u) :=
-- Eq.mpr (id ((insert_emptyc_eq (#u ||| #v)).symm ▸ Eq.refl (Sequent {#u ||| #v} (#v ||| #u))))
--   (Sequent.OrE
--     (Sequent.OrI2
--       (Sequent.Ax
--         (of_eq_true (((congrArg (Membership.mem #u) (insert_emptyc_eq #u)).trans _auxLemma.1).trans (eq_self #u)))))
--     (Sequent.OrI1
--       (Sequent.Ax
--         (of_eq_true (((congrArg (Membership.mem #v) (insert_emptyc_eq #v)).trans _auxLemma.1).trans (eq_self #v))))))

isn't very helpful

[Eric Wieser]

(it's easy to write your own function in CoreM that gives that output, but presumably you don't want the Eq.mprs?

[Thomas Vigouroux]

Well it kinda is, but let's say I'd like to output to be:

u || v |- v || u by OrE
. u |- v || u by OrI2
  u |- u by Ax
. v |- v || u by OrI1
  v |- v by Ax

[Thomas Vigouroux]

I think you understood what I meant

[Eric Wieser]

I think inductive Sequent : Finset Formula → Formula → Type is going to be the best approach here

[Eric Wieser]

You can maybe have both

inductive SequentData : Finset Formula → Formula → Type
inductive Sequent : Finset Formula → Formula → Prop

with the same constructors, and then hopefully show that the former implies the latter

[Yakov Pechersky]

It seems like the desired output more closely matches the tactic steps and the goal state at each step. That would also result in the desired outcome of different tactic proofs for the same proposition giving different outputs. Would it be possible to have a tactic that records the tactics used during a proof which makes this record available elsewhere?

[Thomas Vigouroux]

Changing to -> Type typecheks (and I have proofs about soundness and related), so I guess that's good

[Thomas Vigouroux]

Okay but now it complains about depending on lemmas which don't have executable code

[Thomas Vigouroux]

Nvm, I just had to change to def

[Thomas Vigouroux]

It works great now, that you very much !

[Notification Bot]

Thomas Vigouroux has marked this topic as resolved.

[Thomas Vigouroux]

Sorry to bother again, but in the process I'd like to print out a Finset Formula.
I am fine with the order changing, apparently it requires me to use choice which I don't want, how would I do ?

[Thomas Vigouroux]

My first guess was to do something like

def finsetFmlToString: Finset Formula → String
| ∅ => ""
| insert A ∅ => A.toString
| insert A S => A.toString ++ ", " ++ S.toString

But that does not work because insert is not a match pattern

[Yaël Dillies]

A Finset is a List without duplicate, quotiented out by permutation. Hence it is an element of a quotient of a thing you can print.

[Thomas Vigouroux]

While I follow to theory, I'm not sure about the steps to go from that to an actual working conversion from Finset to String...

[Yaël Dillies]

I mean, have you tried it? #print your_finset

[Thomas Vigouroux]

yeah

[Thomas Vigouroux]

That works, but how do I get the actual value so that I can manipulate it ?

[Yaël Dillies]

docs#repr

[Thomas Vigouroux]

Well... unsafe instance Finset.instReprFinset

[Yaël Dillies]

What do you mean?

[Thomas Vigouroux]

Because it is unsafe I cannot use it in any other block that unsafe ?

[Yaël Dillies]

And that's fine, right? You're trying to prove things about it.

[Thomas Vigouroux]

Well not really, I'm really just wanting to get it to dump the value

[Thomas Vigouroux]

I'm not using it to any other thing than dumping it to the screen

[Yaël Dillies]

So unsafe is fine and there's no reason to be scared.

[Thomas Vigouroux]

Yaël Dillies said:

So unsafe is fine and there's no reason to be scared.

I realized it as I was typing it :wink:

Thanks for your help !

[Thomas Vigouroux]

Okay, so I think I've got something working !

The following proof

def Sequent.orComm: {#u ||| #v} ⊢ #v ||| #u := by {
  rw [← insert_emptyc_eq]
  apply OrE
  · apply OrI2
    apply Ax
    simp only [insert_emptyc_eq, Finset.mem_singleton]
  · apply OrI1
    apply Ax
    simp only [insert_emptyc_eq, Finset.mem_singleton]
}

Dumps the following derivation:

{(u | v)} |- (v | u) OrE
  {u} |- (v | u) OrIR
  {u} |- u.

  {v} |- (v | u) OrIL
  {v} |- v.

[Yakov Pechersky]

def finsetFmlToString: Finset Formula → String := fun s => (s.image (fun A => A.toString)).sort.intercalate ", "

[Thomas Vigouroux]

Little remark though, now that I have the dumping algorithm done, I can create a binary that just dumps a derivation

Sadly that binary is 91M, which seems huge.
Is there a way to reduce the binary size?

[Thomas Vigouroux]

Okay so it turns out that the fact that I changed to -> Type is a little anoying when doing proofs.

Is there any other way to get around that ? Furthermore, I have trouble understanding why this proble arises in the first place, is there any reason why one could not eliminate a T -> Prop to anything other than Prop ?

[Notification Bot]

Thomas Vigouroux has marked this topic as unresolved.

[Yaël Dillies]

There's one reason: it's inconsistent. :point_down:
Yaël Dillies said:

Here's an example of what Eric is saying: If h : p ∨ q, you can't say "Oh I'll map h to 0 if it came from p and to 1 if it came from q" because it could come from both p and q!

[Thomas Vigouroux]

Oh, right

[Thomas Vigouroux]

So then, I have to just work around that in my proofs, right ?

[Yaël Dillies]

I don't really know. It seems you're confusing proving and printing.

[Thomas Vigouroux]

How so?
Printing is just actually showing the object to the screen, proving is about constructing functions to build my objects, right?

[Eric Wieser]

Do you have an example of a proof where Type gets in the way?

[Thomas Vigouroux]

Eric Wieser said:

Do you have an example of a proof where Type gets in the way?

Yup, give me a sec and I'll send it here

[Eric Wieser]

It sounds like the problem is that there are proof steps that aren't actually part of your inductive type (eg Eq.mpr), and you're having to choose between having them appear in the print output, or not using them in the proofs

[Thomas Vigouroux]

Hmm there's probably that

[Thomas Vigouroux]

I'll send you the example in a few minutes

[Thomas Vigouroux]

So basically I have this:

import Lseq.Basic
import Mathlib.Algebra.BigOperators.Basic

section Completeness

def Formula.weight: Formula → ℕ
| ⊥ | #_ => 0
| A &&& B | A ⟹ B => 1 + A.weight + B.weight
| A ||| B => 2 + A.weight + B.weight

def setWeight (S: Finset Formula): ℕ := S.sum Formula.weight

def zeroWeight (hC: C.weight = 0) (hΓ: setWeight Γ = 0): Γ ⊢ C := by {
  cases C with
  | bot => {
    have Γne : Γ.Nonempty
    · sorry
    /-
    tactic 'cases' failed, nested error:
    tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop

    case bot
    Γ: Finset Formula
    hΓ: setWeight Γ = 0
    h: Γ ⊨ Formula.bot
    hC: Formula.weight Formula.bot = 0
    Γne: Finset.Nonempty Γ
    x✝: ∃ x, x ∈ Γ
    ⊢ Sequent Γ Formula.bot
    -/
    obtain ⟨A, hA⟩ := Finset.Nonempty.bex Γne
  }
  | var _ => sorry
  | and _ _
  | or _ _
  | imp _ _ => {
    simp [Formula.weight] at hC
  }
}

end Completeness

I have removed some hypothesis (thus the sorry in the have)

[Thomas Vigouroux]

(The actual proof does not work, but that's not the question here, right ?)

[Eric Wieser]

Ah, what you're seeing here is that by changing Prop into Type, you are now forcing yourself to use only constructive proofs (in a much stronger sense than usual); so using Finset.Nonempty isn't going to work for you, as you can't use it to "construct" a witness

[Eric Wieser]

Note the above isn't a #mwe as Lseq.Basic doesn't exist for me

[Thomas Vigouroux]

Oh, right, sorry for that!
So I have to construct it manually then, right?

[Thomas Vigouroux]

Oh okay, so I have found Finset.choose which seems to help a litle, but my problem is that I can prove existence but now unicity...

[Kyle Miller]

Why is it that it's necessary to try to work with this inductive type as a Type? Tactics are themselves programs that manipulate the Exprs representing a terms, with no need to have the terms be able to be evaluated. (For example, the tauto tactic is able to automatically prove classical propositional logic.)

If you really need to output terms and leave Lean, in principle you should be able to take a theorem and output a derivation. It will take some figuring out for how to transform the proof terms into the desired output.

Something that's related is #explode, which is like #print but gives Fitch-style proof tables. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Explode.html

[Kyle Miller]

I guess you said you wanted to do intuitionistic propositional logic -- maybe using Prop is cheating, since it allows you to use classical logic to prove Sequents exist

[Thomas Vigouroux]

I am not sure I follow what you mean