Skip to content

Remove unused newFacts and newObjects #39

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
PatrickMassot merged 1 commit into from
Jul 23, 2026
Merged

Remove unused newFacts and newObjects #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
114 changes: 0 additions & 114 deletions Verbose/English/Common.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,120 +62,6 @@ def listMaybeTypedIdentToNewStuffSuchThatEN : List MaybeTypedIdent → MetaM (TS
| [x, y, z] => do `(newStuff| $(← x.stx):maybeTypedIdent such that $(← y.stx) and $(← z.stx))
| _ => pure default

declare_syntax_cat newFacts
syntax colGt namedType : newFacts
syntax colGt namedType " and " colGt namedType : newFacts
syntax colGt namedType ", " colGt namedType " and " colGt namedType : newFacts

def newFactsToArray : TSyntax `newFacts → Array NamedType
| `(newFacts| $x:namedType) => #[toNamedType x]
| `(newFacts| $x:namedType and $y:namedType) =>
#[toNamedType x, toNamedType y]
| `(newFacts| $x:namedType, $y:namedType and $z:namedType) =>
#[toNamedType x, toNamedType y, toNamedType z]
| _ => #[]

def newFactsToTypeTerm : TSyntax `newFacts → MetaM Term
| `(newFacts| $x:namedType) => do
namedTypeToTypeTerm x
| `(newFacts| $x:namedType and $y) => do
let xT ← namedTypeToTypeTerm x
let yT ← namedTypeToTypeTerm y
`($xT ∧ $yT)
| `(newFacts| $x:namedType, $y:namedType and $z) => do
let xT ← namedTypeToTypeTerm x
let yT ← namedTypeToTypeTerm y
let zT ← namedTypeToTypeTerm z
`($xT ∧ $yT ∧ $zT)
| _ => throwError "Could not convert the description of new facts into a term."

open Tactic Lean.Elab.Tactic.RCases in
def newFactsToRCasesPatt : TSyntax `newFacts → RCasesPatt
| `(newFacts| $x:namedType) => namedTypeListToRCasesPatt [x]
| `(newFacts| $x:namedType and $y:namedType) => namedTypeListToRCasesPatt [x, y]
| `(newFacts| $x:namedType, $y:namedType and $z:namedType) => namedTypeListToRCasesPatt [x, y, z]
| _ => default

def listMaybeTypedIdentToNewFacts : List MaybeTypedIdent → MetaM (TSyntax `newFacts)
| [x] => do `(newFacts| $(.mk (← x.stx)))
| [x, y] => do `(newFacts| $(.mk (← x.stx).raw):namedType and $(.mk (← y.stx)))
| [x, y, z] => do `(newFacts| $(.mk (← x.stx)):namedType, $(.mk (← y.stx)) and $(.mk (← z.stx)))
| _ => pure default

declare_syntax_cat newObject
syntax maybeTypedIdent "such that " maybeTypedIdent : newObject
syntax maybeTypedIdent "such that " maybeTypedIdent colGt " and " maybeTypedIdent : newObject
syntax maybeTypedIdent "such that " maybeTypedIdent ", " colGt maybeTypedIdent colGt " and " maybeTypedIdent : newObject

syntax maybeTypedIdent " and " maybeTypedIdent "such that " maybeTypedIdent : newObject
syntax maybeTypedIdent " and " maybeTypedIdent "such that " maybeTypedIdent colGt " and " maybeTypedIdent : newObject
syntax maybeTypedIdent " and " maybeTypedIdent "such that " maybeTypedIdent ", " colGt maybeTypedIdent colGt " and " maybeTypedIdent : newObject

def newObjectToTerm : TSyntax `newObject → MetaM Term
| `(newObject| $x:maybeTypedIdent such that $new) => do
let x' ← maybeTypedIdentToExplicitBinder x
-- TODO Better error handling
let newT := (toMaybeTypedIdent new).2.get!
`(∃ $(.mk x'), $newT)
| `(newObject| $x:maybeTypedIdent such that $new₁ and $new₂) => do
let x' ← maybeTypedIdentToExplicitBinder x
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
`(∃ $(.mk x'), $new₁T ∧ $new₂T)
| `(newObject| $x:maybeTypedIdent such that $new₁, $new₂ and $new₃) => do
let x' ← maybeTypedIdentToExplicitBinder x
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
let new₃T := (toMaybeTypedIdent new₃).2.get!
`(∃ $(.mk x'), $new₁T ∧ $new₂T ∧ $new₃T)
| `(newObject| $x:maybeTypedIdent and $y:maybeTypedIdent such that $new) => do
let x' ← maybeTypedIdentToExplicitBinder x
let y' ← maybeTypedIdentToExplicitBinder y
-- TODO Better error handling
let newT := (toMaybeTypedIdent new).2.get!
`(∃ $(.mk x'), ∃ $(.mk y'), $newT)
| `(newObject| $x:maybeTypedIdent and $y:maybeTypedIdent such that $new₁ and $new₂) => do
let x' ← maybeTypedIdentToExplicitBinder x
let y' ← maybeTypedIdentToExplicitBinder y
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
`(∃ $(.mk x'), ∃ $(.mk y'), $new₁T ∧ $new₂T)
| `(newObject| $x:maybeTypedIdent and $y:maybeTypedIdent such that $new₁, $new₂ and $new₃) => do
let x' ← maybeTypedIdentToExplicitBinder x
let y' ← maybeTypedIdentToExplicitBinder y
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
let new₃T := (toMaybeTypedIdent new₃).2.get!
`(∃ $(.mk x'), ∃ $(.mk y'), $new₁T ∧ $new₂T ∧ $new₃T)
| _ => throwError "Could not convert the new object description into a term."

def newObjectToMaybeTypedIdentList : TSyntax `newObject → List (TSyntax `maybeTypedIdent)
| `(newObject| $x:maybeTypedIdent such that $new) => [x, new]
| `(newObject| $x:maybeTypedIdent such that $new₁ and $new₂) => [x, new₁, new₂]
| `(newObject| $x:maybeTypedIdent such that $new₁, $new₂ and $new₃) => [x, new₁, new₂, new₃]
| `(newObject| $x:maybeTypedIdent and $y:maybeTypedIdent such that $new) => [x, y, new]
| `(newObject| $x:maybeTypedIdent and $y:maybeTypedIdent such that $new₁ and $new₂) => [x, y, new₁, new₂]
| `(newObject| $x:maybeTypedIdent and $y:maybeTypedIdent such that $new₁, $new₂ and $new₃) => [x, y, new₁, new₂, new₃]
| _ => []


def newObjectToArray : TSyntax `newObject → Array MaybeTypedIdent
| `(newObject| $x:maybeTypedIdent such that $news:maybeTypedIdent) =>
Array.map toMaybeTypedIdent #[x, news]
| `(newObject| $x:maybeTypedIdent such that $y:maybeTypedIdent and $z) =>
Array.map toMaybeTypedIdent #[x, y, z]
| _ => #[]

open Tactic Lean.Elab.Tactic.RCases in
def newObjectToRCasesPatt (newObj : TSyntax `newObject) : RCasesPatt :=
maybeTypedIdentListToRCasesPatt <| newObjectToMaybeTypedIdentList newObj

-- FIXME: the code below is ugly, written in a big hurry.
def listMaybeTypedIdentToNewObject : List MaybeTypedIdent → MetaM (TSyntax `newObject)
| [x, y] => do `(newObject| $(← x.stx):maybeTypedIdent such that $(← y.stx'))
| [x, y, z] => do `(newObject| $(← x.stx):maybeTypedIdent such that $(← y.stx) and $(← z.stx))
| _ => pure default

declare_syntax_cat facts
syntax term : facts
syntax term " and " term : facts
Expand Down
114 changes: 0 additions & 114 deletions Verbose/French/Common.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,122 +61,8 @@ def listMaybeTypedIdentToNewStuffSuchThatFR : List MaybeTypedIdent → MetaM (TS
| [x, y, z] => do `(newStuffFR| $(← x.stx):maybeTypedIdent tel que $(← y.stx) et $(← z.stx))
| _ => pure default

declare_syntax_cat newFactsFR
syntax colGt namedType : newFactsFR
syntax colGt namedType " et " colGt namedType : newFactsFR
syntax colGt namedType ", " colGt namedType " et " colGt namedType : newFactsFR

def newFactsFRToArray : TSyntax `newFactsFR → Array NamedType
| `(newFactsFR| $x:namedType) => #[toNamedType x]
| `(newFactsFR| $x:namedType et $y:namedType) =>
#[toNamedType x, toNamedType y]
| `(newFactsFR| $x:namedType, $y:namedType et $z:namedType) =>
#[toNamedType x, toNamedType y, toNamedType z]
| _ => #[]

def newFactsFRToTypeTerm : TSyntax `newFactsFR → MetaM Term
| `(newFactsFR| $x:namedType) => do
namedTypeToTypeTerm x
| `(newFactsFR| $x:namedType et $y) => do
let xT ← namedTypeToTypeTerm x
let yT ← namedTypeToTypeTerm y
`($xT ∧ $yT)
| `(newFactsFR| $x:namedType, $y:namedType et $z) => do
let xT ← namedTypeToTypeTerm x
let yT ← namedTypeToTypeTerm y
let zT ← namedTypeToTypeTerm z
`($xT ∧ $yT ∧ $zT)
| _ => throwError "N'a pas pu convertir la description des nouveaux faits en un terme."

open Tactic Lean.Elab.Tactic.RCases in
def newFactsFRToRCasesPatt : TSyntax `newFactsFR → RCasesPatt
| `(newFactsFR| $x:namedType) => namedTypeListToRCasesPatt [x]
| `(newFactsFR| $x:namedType et $y:namedType) => namedTypeListToRCasesPatt [x, y]
| `(newFactsFR| $x:namedType, $y:namedType et $z:namedType) => namedTypeListToRCasesPatt [x, y, z]
| _ => default

def listMaybeTypedIdentToNewFactsFR : List MaybeTypedIdent → MetaM (TSyntax `newFactsFR)
| [x] => do `(newFactsFR| $(.mk (← x.stx)))
| [x, y] => do `(newFactsFR| $(.mk (← x.stx).raw):namedType et $(.mk (← y.stx)))
| [x, y, z] => do `(newFactsFR| $(.mk (← x.stx)):namedType, $(.mk (← y.stx)) et $(.mk (← z.stx)))
| _ => pure default

syntax telsQue := "tel que " <|> "tels que "

declare_syntax_cat newObjectFR
syntax maybeTypedIdent "tel que " maybeTypedIdent : newObjectFR
syntax maybeTypedIdent "tel que " maybeTypedIdent colGt " et " maybeTypedIdent : newObjectFR
syntax maybeTypedIdent "tel que " maybeTypedIdent ", " colGt maybeTypedIdent colGt " et " maybeTypedIdent : newObjectFR

syntax maybeTypedIdent " et " maybeTypedIdent telsQue maybeTypedIdent : newObjectFR
syntax maybeTypedIdent " et " maybeTypedIdent telsQue maybeTypedIdent colGt " et " maybeTypedIdent : newObjectFR
syntax maybeTypedIdent " et " maybeTypedIdent telsQue maybeTypedIdent ", " colGt maybeTypedIdent colGt " et " maybeTypedIdent : newObjectFR

def newObjectFRToTerm : TSyntax `newObjectFR → MetaM Term
| `(newObjectFR| $x:maybeTypedIdent tel que $new) => do
let x' ← maybeTypedIdentToExplicitBinder x
-- TODO Better error handling
let newT := (toMaybeTypedIdent new).2.get!
`(∃ $(.mk x'), $newT)
| `(newObjectFR| $x:maybeTypedIdent tel que $new₁ et $new₂) => do
let x' ← maybeTypedIdentToExplicitBinder x
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
`(∃ $(.mk x'), $new₁T ∧ $new₂T)
| `(newObjectFR| $x:maybeTypedIdent tel que $new₁, $new₂ et $new₃) => do
let x' ← maybeTypedIdentToExplicitBinder x
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
let new₃T := (toMaybeTypedIdent new₃).2.get!
`(∃ $(.mk x'), $new₁T ∧ $new₂T ∧ $new₃T)
| `(newObjectFR| $x:maybeTypedIdent et $y:maybeTypedIdent $_:telsQue $new) => do
let x' ← maybeTypedIdentToExplicitBinder x
let y' ← maybeTypedIdentToExplicitBinder y
-- TODO Better error handling
let newT := (toMaybeTypedIdent new).2.get!
`(∃ $(.mk x'), ∃ $(.mk y'), $newT)
| `(newObjectFR| $x:maybeTypedIdent et $y:maybeTypedIdent tel que $new₁ et $new₂) => do
let x' ← maybeTypedIdentToExplicitBinder x
let y' ← maybeTypedIdentToExplicitBinder y
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
`(∃ $(.mk x'), ∃ $(.mk y'), $new₁T ∧ $new₂T)
| `(newObjectFR| $x:maybeTypedIdent et $y:maybeTypedIdent tel que $new₁, $new₂ et $new₃) => do
let x' ← maybeTypedIdentToExplicitBinder x
let y' ← maybeTypedIdentToExplicitBinder y
let new₁T := (toMaybeTypedIdent new₁).2.get!
let new₂T := (toMaybeTypedIdent new₂).2.get!
let new₃T := (toMaybeTypedIdent new₃).2.get!
`(∃ $(.mk x'), ∃ $(.mk y'), $new₁T ∧ $new₂T ∧ $new₃T)
| _ => throwError "N'a pas pu convertir la description du nouvel object en un terme."

def newObjectFRToMaybeTypedIdentList : TSyntax `newObjectFR → List (TSyntax `maybeTypedIdent)
| `(newObjectFR| $x:maybeTypedIdent tel que $new) => [x, new]
| `(newObjectFR| $x:maybeTypedIdent tel que $new₁ et $new₂) => [x, new₁, new₂]
| `(newObjectFR| $x:maybeTypedIdent tel que $new₁, $new₂ et $new₃) => [x, new₁, new₂, new₃]
| `(newObjectFR| $x:maybeTypedIdent et $y:maybeTypedIdent $_ $new) => [x, y, new]
| `(newObjectFR| $x:maybeTypedIdent et $y:maybeTypedIdent $_ $new₁ et $new₂) => [x, y, new₁, new₂]
| `(newObjectFR| $x:maybeTypedIdent et $y:maybeTypedIdent $_ $new₁, $new₂ et $new₃) => [x, y, new₁, new₂, new₃]
| _ => []


def newObjectFRToArray : TSyntax `newObjectFR → Array MaybeTypedIdent
| `(newObjectFR| $x:maybeTypedIdent tel que $news:maybeTypedIdent) =>
Array.map toMaybeTypedIdent #[x, news]
| `(newObjectFR| $x:maybeTypedIdent tel que $y:maybeTypedIdent et $z) =>
Array.map toMaybeTypedIdent #[x, y, z]
| _ => #[]

open Tactic Lean.Elab.Tactic.RCases in
def newObjectFRToRCasesPatt (newObj : TSyntax `newObjectFR) : RCasesPatt :=
maybeTypedIdentListToRCasesPatt <| newObjectFRToMaybeTypedIdentList newObj

-- FIXME: the code below is ugly, written in a big hurry.
def listMaybeTypedIdentToNewObjectFR : List MaybeTypedIdent → MetaM (TSyntax `newObjectFR)
| [x, y] => do `(newObjectFR| $(← x.stx):maybeTypedIdent tel que $(← y.stx'))
| [x, y, z] => do `(newObjectFR| $(← x.stx):maybeTypedIdent tel que $(← y.stx) et $(← z.stx))
| _ => pure default

declare_syntax_cat factsFR
syntax term : factsFR
syntax term " et " term : factsFR
Expand Down