So I have a file in coq, which is a bit like the following:
Section S.
Context (a : TA).
Context (b : TA → TB).
Definition X : TB.
Proof.
apply b.
exact a.
Defined.
Context (c : TB → TC).
Definition Y : TC.
Proof.
apply c.
exact X.
Defined.
End S.
This file is growing very large, which means waiting a long time if I add an import statement and then start working at the bottom of the file. Therefore, I thought I'd split it up into smaller files. However, when I split the section into smaller sections, these sections don't share their context...
Section S.
Context (a : TA).
Context (b : TA → TB).
Definition X : TB.
Proof.
apply b.
exact a.
Defined.
End S.
Section T.
Context (a : TA).
Context (b : TA → TB).
Context (c : TB → TC).
Definition Y : TC.
Proof.
apply c.
exact X. (* Error: The term "X" has type "TA → (TA → TB) → TB" while it is expected to have type "TB". *)
Defined.
End T.
...so if I want to use definitions and lemmas from a previous section, I will need to manually provide these context variables every time (X a b instead of X) and this will grow unreadable and cumbersome quite quickly. So is there a way to either
- tell coq that one section is merely a continuation of another,
- or to say "for the definitions from section
S, fill in the valuesaandbfor their argumentsaandb"?
