Fix Quot and Eq names for Lean 4 compatibility

[Copilot]

Lean 4 exports use Quot and Eq (capital letters) for quotient and equality types, but the importer was hardcoded to quot and eq (lowercase) from Lean 3. This caused "missing Quot" errors and type mismatch errors when importing Lean 4 files.

Changes:

Quot changes:

• leanParse.ml: Updated quot_name from "quot" to "Quot"
• Lean.v: Updated all Register statements from lean.quot.* to lean.Quot.*
• lean.ml: Updated the has_ref check from "lean.quot" to "lean.Quot"

Eq changes:

• Lean.v: Updated Register statements from lean.eq to lean.Eq and lean.eq_inst1 to lean.Eq_inst1
• Lean.v: Added Notation Eq := eq (only parsing). for backwards compatibility
• lean.ml: Updated predeclared name from ["eq"] to ["Eq"]

Tests:

• Added pnni.v test case using the provided Lean 4 export

Example from the failing export:

5 #NS 0 Eq
2692 #NS 0 Quot
2693 #NS 2692 liftOn

Why all these changes are needed:
The declare_quot function in lean.ml constructs registration strings using quot_name: "lean." ^ N.to_lean_string lean. Since quot_name is now "Quot", the Register statements in Lean.v must use lean.Quot.* to match, and the has_ref check must also look for lean.Quot. Similarly, the predeclared inductives lookup uses names from Lean exports, so "eq" must be changed to "Eq" to match Lean 4's naming.

Errors fixed:

Error at line 35053 (for Quot.liftOn): #DEF 2693 31622 31635 17 21
missing Quot

The 5th term has type "forall a b : α, r a b -> Eq β (f a) (f b)"
which should be a subtype of "forall a b : α, r a b -> eq (f a) (f b)".

The parser now correctly recognizes these Quot and Eq names from Lean 4 exports and properly registers them on the Rocq side.

Fixes #44

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Does the importer support Quot</issue_title>
<issue_description>Temp.lean

theorem plus_n_n_injective : ∀ (n m : Nat),
  n + n = m + m →
  n = m := by
  intro n
  induction n with
  | zero =>
    intro m H
    cases m with
    | zero => rfl
    | succ m' => 
      contradiction
  | succ n' IH =>
    intro m
    cases m with
    | zero =>
      intro H
      contradiction
    | succ m' =>
      intro H
      have H2 : n' + n' = m' + m' := by omega
      have H3 : n' = m' := IH m' H2
      rw [H3]

From LeanImport Require Import Lean.
Redirect "Imported.log" Lean Import "pnni.out".

export.txt

Importer errors on the given code.

Error:
Error at line 35053 (for Quot.liftOn): #DEF 2693 31622 31635 17 21
missing Quot

</issue_description>

<agent_instructions>Make sure to add the txt to the test-suite in the right way so the CI will check it</agent_instructions>

Comments on the Issue (you are @copilot in this section)

@JasonGross @SkySkimmer Is the importer supposed to be able to handle `Quot`? Do we need to define this Rocq-side or something? @SkySkimmer It is defined rocq side I think there was something where the name changed between lean 3 and lean 4, we may still be using the lean 3 name? https://github.com/rocq-community/rocq-lean-import/blob/6f72ad437e82b2bb5b3e9f06ffd2dfeffb273d24/src/leanParse.ml#L119 @JasonGross Let's see if @copilot can fix this issue by replacing `quot` with `Quot`

• Fixes Does the importer support Quot #44

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

[JasonGross]

@copilot Changes to Lean.v are not necessary, only change the casing in leanParse.ml, not lean.ml

[Copilot]

@copilot Changes to Lean.v are not necessary, only change the casing in leanParse.ml, not lean.ml

Reverted changes to Lean.v and lean.ml. Only leanParse.ml is modified now. (b40b5f5)

[SkySkimmer]

@copilot Changes to Lean.v are not necessary, only change the casing in leanParse.ml, not lean.ml

I think they were necessary, declare_quot uses quot_name to get the registers

[JasonGross]

I see. Okay, @copilot put back the changes to Lean.v

[Copilot]

I see. Okay, @copilot put back the changes to Lean.v

Restored changes to Lean.v and lean.ml. All three files (leanParse.ml, Lean.v, and lean.ml) are now updated because declare_quot uses quot_name to construct the registration strings "lean." + quot_name, so they all need to be consistent. (04bc7bb)

[JasonGross]

@SkySkimmer I guess we need to rename eq to Eq too?

[JasonGross]

@copilot rename eq to Eq and similar to fix

 Error:
  - Error at line 35053 (for Quot.liftOn): #DEF 2693 31622 31635 17 21
  - Illegal application: 
  - The term "@Quot.lift" of type
  -  "forall (α : Type) (r : α -> α -> SProp) (β : Type) (f : α -> β),
  -   (forall a b : α, r a b -> eq (f a) (f b)) -> Quot.quot r -> β"
  - cannot be applied to the terms
  -  "_UU03b1_" : "Type"
  -  "r" : "_UU03b1_ -> _UU03b1_ -> SProp"
  -  "_UU03b2_" : "Type"
  -  "f" : "_UU03b1_ -> _UU03b2_"
  -  "c" : "forall a b : _UU03b1_, r a b -> Eq _UU03b2_ (f a) (f b)"
  -  "q" : "Quot.quot r"
  - The 5th term has type
  -  "forall a b : _UU03b1_, r a b -> Eq _UU03b2_ (f a) (f b)"
  - which should be a subtype of
  -  "forall a b : _UU03b1_, r a b -> eq (f a) (f b)".

Add Notation eq := Eq (only parsing). for backwards compatibility

[Copilot]

@copilot rename eq to Eq and similar to fix

...

Renamed eq to Eq in both Lean.v (registrations) and lean.ml (predeclared name). Added Notation Eq := eq (only parsing). for backwards compatibility. (4885798)

[JasonGross]

@SkySkimmer does any of the other machinery require the same naming between Rocq and Lean? Do you have any idea why we're importing Eq?

[JasonGross]

@SkySkimmer I think this is a bug in Rocq, or else an issue with how the plugin is ascribing relevance marks:

From LeanImport Require Import Lean.
Lean Import "../dumps/pnni.out" 1 67843.
Goal forall n' m',
@eq Bool
    (Lean_Omega_Constraint_sat'
       (Lean_Omega_tidyConstraint
          (Lean_Omega_Constraint_mk
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero)))
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero))))
          (List_cons_inst1 Int
             (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                (instOfNat (Nat_succ (Nat_succ Nat_zero))))
             (List_cons_inst1 Int
                (Neg_neg_inst1 Int Int_instNegInt
                   (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                      (instOfNat (Nat_succ (Nat_succ Nat_zero)))))
                (List_nil_inst1 Int))))
       (Lean_Omega_tidyCoeffs
          (Lean_Omega_Constraint_mk
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero)))
             (Option_some_inst1 Int
                (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero))))
          (List_cons_inst1 Int
             (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                (instOfNat (Nat_succ (Nat_succ Nat_zero))))
             (List_cons_inst1 Int
                (Neg_neg_inst1 Int Int_instNegInt
                   (OfNat_ofNat_inst1 Int (Nat_succ (Nat_succ Nat_zero))
                      (instOfNat (Nat_succ (Nat_succ Nat_zero)))))
                (List_nil_inst1 Int))))
       (Lean_Omega_Coeffs_ofList
          (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt n')
             (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt m')
                (List_nil_inst1 Int)))))
    Bool_true ->
 @eq Bool
    (Lean_Omega_Constraint_sat'
       (Lean_Omega_Constraint_mk
          (Option_some_inst1 Int
             (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero)))
          (Option_some_inst1 Int
             (OfNat_ofNat_inst1 Int Nat_zero (instOfNat Nat_zero))))
       (List_cons_inst1 Int
          (OfNat_ofNat_inst1 Int (Nat_succ Nat_zero)
             (instOfNat (Nat_succ Nat_zero)))
          (List_cons_inst1 Int
             (Neg_neg_inst1 Int Int_instNegInt
                (OfNat_ofNat_inst1 Int (Nat_succ Nat_zero)
                   (instOfNat (Nat_succ Nat_zero))))
             (List_nil_inst1 Int)))
       (Lean_Omega_Coeffs_ofList
          (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt n')
             (List_cons_inst1 Int (Nat_cast_inst1 Int instNatCastInt m')
                (List_nil_inst1 Int)))))
    Bool_true.
    intros n' m'.
    Fail intro x; exact x. (* type mismatch *)
    cbv. (* Alt: cbn. cbv [Lean_Omega_Constraint_div]. *)
    intro x; exact x. (* success *)
Fail Qed.