Comments (2)
I experimented with this a bit:
Tactic Notation "lhs" tactic3(tac) :=
let R := match goal with |- ?R _ _ => constr:(R) end in
let pre_transitivity_proof_term_head := constr:(_ : Transitive R) in
let transitivity_proof_term_head := (eval hnf in pre_transitivity_proof_term_head) in
nrefine (pre_transitivity_proof_term_head _ _ _ ltac:(tac) _).
It didn't work out too well for the following reasons:
- Doing a typeclass search every time is a lot of wasted work.
- In some situations we implicitly assume that the goal will resolve to
paths
. - The universe levels cause unification issues.
- The proof terms are a bit more complex.
My next suggestion would be to hard code the transitivity proofs for each kind of relation we want this to work on in order to solve (1) but then we get stuck on (2).
(3) is really tricky to understand when things go wrong.
(4) isn't great as Coq spends more and more time unfolding terms that it shouldn't need to.
We could instead introduce variants of lhs
like lhsE
for Equiv,
lhsC` for wildcat etc. That way we wouldn't have issues 1-4, however then we would have even more tactics.
from coq-hott.
Can you explain more?
- I would assume that the typeclass search should be very fast, since in every case where we would use this, the instance should be obvious.
- I don't understand what you mean here.
- Can you give an example? Why are there universe issues with this?
- Can you give an example? It looks to me like it should give a very similar proof term.
from coq-hott.
Related Issues (20)
- Work out why test/WildCat/Opposite.v is slow HOT 2
- Remove redundant fields from Ring
- Define matrices as functions HOT 2
- Define matrices as a collection of columns rather than a collection of rows
- General Linear group HOT 1
- Finite fields (Galois fields)
- Prime numbers
- Idempotent ring elements
- grp_pow and related things HOT 9
- Tensor product of cyclic groups HOT 26
- use CongruenceQuotient to define coequalizer HOT 9
- Error: Unknown scope delimiting key _type. HOT 6
- Coq Platform and opam version lags HOT 5
- Add HasEquivs instance for MatrixCat HOT 1
- Binomial Coefficients
- Replace old definition of `cyclic` with new `cyclic'`
- Fundamental theorem of arithmetic HOT 1
- Add functorality of cokernels and quotients for AbGroup
- Allow subgroups to be defined by predicates that don't take values in h-props
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-hott.