A proof assistant for general type theories
Home Page: http://www.andromeda-prover.org/
License: Other
Andromeda is a prover for dependent type theories à la Martin-Löf.
See the official Andromeda web site for more information, such as installation instructions and links to the ICFP 2019 materials.
I would like to try my hand at writing auto for Brazilians. (I think I can get a valid term inference by by introducing a false axiom to get the process started, but I'm not sure how to get the constructed term out without having access to some kind of inference or unification on the term level, e.g., a type_of operator that will take a term t :: T and give me back T.) (Also, I want to try my hand at computing with funext.) Which branch should I use? The master branch seems to be missing evil.tt (for the smoketest), and has some files in examples/ which seem to use the old syntax. But when I try to compile on the tt2 branch using caml-shift delimcc, I get
$ make
ocamlbuild -lib unix -use-menhir -menhir "menhir --explain" -cflags -g,-annot,"-warn-error +a" -use-ocamlfind -pkgs delimcc brazil.byte
+ ocamlfind ocamldep -package delimcc -modules brazil/brazil.ml > brazil/brazil.ml.depends
ocamlfind: Package `delimcc' not found
Command exited with code 2.
Compilation unsuccessful after building 1 target (0 cached) in 00:00:00.
Makefile:15: recipe for target 'brazil.byte' failed
make: *** [brazil.byte] Error 10
So which branch should I be using (or should I come back in a week or a month or later and try again then)?
(Also, do you want a travis config file for travis to do CI for you?)
At https://github.com/andrejbauer/tt/blob/master/tt.ml#L100, the types and expressions in the declarations from ctx.decls should be shifted based on their position in the context. This is done by Context.lookup_ty, but not by Context.decls.
The equations returned by context joins are ignored, and moreover context join always returns an empty list of equations. It is better to remove them. We will put them back in when we know what to do with them (right now they get addded to the context).
We should have better names for different kinds of hints:
beta could be rewrite or calculateeta be?Also, the current system of installing and uninstalling hints by tagging them can be replaced with somethign more flexible (and less annoying), as follows. We can still install hints, but rather than uninstalling them with unhint or whatever we block specific hints by providing patterns. Example: suppose we defined natural numbers and installed standard beta hints for computing +, * and exponentials ^. We would like to prove that 2 ^ (2 ^ (2 ^ (2 ^ 2))) is even. It is a bad idea to reduce this term, so we block it by saying something like:
block beta 2 ^ (2 ^ (2 ^ (2 ^ 2))) in ...
or more generally, if we want to block every power of two:
block beta (lambda [n : N] 2 ^ n) in ...
Eta hints could be blocked by specifying the blocking type, e.g. to prevent eta hints on anythin of the form unit * A we could write
block eta (lambda [A : Type] unit * A) in ...
Something similar might work for genertal hints.
Would it be possible to avoid large type annotations by turning "non-tricky" applications into spines which have a single type annotation on the head?
For instance, in
f x y z
the type annotation on f already determines everything. There is no need to have further type annotations on f x and f x y, of course assuming we're not in a funny case where some equation screwed up everything.
In general it seems we should be shooting for a sytem that works well in case there are no funny equations running around (such as nat -> bool == nat -> nat). Somehow we need two notions of type: the "expected" type and the "given type".
Then perhaps the given types can be always explicitly given with type ascriptions?
This sort of thinking probably leads to some problems regarding rewriting and pattern matching. An example to keep in mind:
Parameter e : nat -> bool == nat -> nat.
Definition f : nat -> bool := (fun _ : nat => false).
Definition x := 42 + (equation e in (f :: nat -> nat)) 0.
Here x is strange. We should not reduce it to 42 + false. I wonder how this works in brazil right now. Does equation e in ... get thrown away by typing.ml? Hopefully not.
Definition Type := Universe f0.
Parameter bool : Type.
Parameter true false : bool.
Definition contr_true_inhab := ({ 1 = true ; 2 = idpath true } :: { 1 : bool ; 2 : 1 = true }).gives
$ ./brazil.native sig.br
Type is defined.
bool is assumed.
true is assumed.
false is assumed.
Typing error: sig.br:6:33: expression {1 = true; 2 = idpath true} has type
{1 as 1 : bool; 2 as 2 : true = true}
but should have type {1: bool; 2: 1 = true}
Are we planning to merge brasil-merge to master soon? Since master is in a sorry state anyway, we might as well do it.
I would like to propose that the output from the pretty printer should be parsable. We can just ignore the annotations during parsing. The other issue is how to deal with the difference between a type and the type named by an element. When annotations are turned on with Print.annotate, El is printed explicitly, but that cannnot be parsed. Maybe we can just add El to the parser.
If Tt.abstract functions are always called from the outside at level 0 then we could change the signature of these functions so that we do not have to provide the level every time.
@christopherastone, is the tentatively business still useful? It looks like a big hack to me.
One of the recent commits broke check_fst_fst; it now gives
Warning: <<850>>Why are applications
sigma_elim (sigma X Q) R (pair (sigma X Q) R (pair X Q x y) z)
(fun (_ : sigma (sigma X Q) R) => sigma X Q)
(fun (a : sigma X Q) (_0 : R a) => a)
and
pair X Q x y
equal?
Warning: <<854>>Why are applications
sigma_elim (sigma X Q) R (pair (sigma X Q) R (pair X Q x y) z)
(fun (_ : sigma (sigma X Q) R) => sigma X Q)
(fun (a : sigma X Q) (_0 : R a) => a)
and
pair X Q x y
equal?
Warning: <<858>>Why are applications
sigma_elim (sigma X Q) R (pair (sigma X Q) R (pair X Q x y) z)
(fun (_ : sigma (sigma X Q) R) => sigma X Q)
(fun (a : sigma X Q) (_0 : R a) => a)
and
pair X Q x y
equal?
Warning: <<862>>Why are applications
sigma_elim (sigma X Q) R (pair (sigma X Q) R (pair X Q x y) z)
(fun (_ : sigma (sigma X Q) R) => sigma X Q)
(fun (a : sigma X Q) (_0 : R a) => a)
and
pair X Q x y
equal?
Warning: <<864>>Why are terms
x
and
sigma_elim X Q
(fst (sigma X Q) R (pair (sigma X Q) R (pair X Q x y) z))
(fun (_ : sigma X Q) => X) (fun (a : X) (_ : Q a) => a)
equal?
Typing error: examples/sigma.br:81:3: expression refl x has type x == x
but should have type fst X Q
(fst (sigma X Q) R (pair (sigma X Q) R (pair X Q x y) z))
==
x
Whether or not sigma bool (fun (b : bool) => b = true) == sigma bool (fun (b : bool) => b = false) is consistent depends on whether we axiomatize sigma types, or define them with records.
Definition Type := Universe f0.
Parameter bool : Type.
Parameter true false : bool.
Parameter bool_ind :
forall (P : bool -> Type) (b : bool), P true -> P false -> P b.
Parameter bool_ind_false :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P false x y == y.
Parameter bool_ind_true :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P true x y == x.
Rewrite bool_ind_true.
Rewrite bool_ind_false.
Definition cond := fun (A : Type) => bool_ind (fun (C : bool) => A).
Definition cond_false :=
fun (A : Type) (x : A) (y : A) =>
(refl y :: bool_ind (fun U : bool => A) false x y == y).
Definition cond_true :=
fun (A : Type) (x : A) (y : A) =>
(refl x :: bool_ind (fun V : bool => A) true x y == x).
Definition or := fun (a b : bool) => cond bool a true b.
Definition and := fun (a b : bool) => cond bool a b false.
(*Definition prodR := fun (A B : Type) => { fst : A ; snd : B }.
Definition pairR := fun (A B : Type) (a : A) (b : B) => ({ fst = a ; snd = b } :: prodR A B).
Definition fstR := fun (A B : Type) (x : prodR A B) => (x.fst :: A).
Definition sndR := fun (A B : Type) (x : prodR A B) => (x.snd :: B).*)
Definition sigmaR := fun (A : Type) (P : A -> Type) => { fst : A ; snd : P fst }.
Definition pairR := fun (A : Type) (P : A -> Type) (x : A) (p : P x)
=> { fst = x ; snd = (p :: P fst) } :: sigmaR A P.
Parameter sigma : forall (A : Type), (A -> Type) -> Type.
Parameter pair :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a),
sigma A P.
Parameter sigma_elim :
forall (A : Type)
(P : A -> Type)
(u : sigma A P)
(C : sigma A P -> Type),
(forall (a : A) (b : P a), C (pair A P a b)) -> C u.
Parameter sigma_beta :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a)
(C : sigma A P -> Type)
(f : forall (a : A) (b : P a), C (pair A P a b)),
sigma_elim A P (pair A P a b) C f == f a b.
Parameter sigma_comm :
forall (A : Type)
(P : A -> Type)
(Q : sigma A P -> Type)
(q : forall (x : A) (p : P x), Q (pair A P x p))
(R : forall (x : sigma A P), Q x -> Type)
(f : forall (x : sigma A P) (q : Q x), R x q)
(u : sigma A P),
rewrite sigma_beta in
sigma_elim A P u
(fun (x : sigma A P) => R x (sigma_elim A P x Q (fun (x : A) (p : P x) => q x p)))
(fun (x : A) (p : P x) => f (pair A P x p) (q x p) :: R (pair A P x p) (sigma_elim A P (pair A P x p) Q q))
==
f u (sigma_elim A P u Q q).
Definition sigma_half_eta :=
fun (A : Type)
(P : A -> Type)
(u : sigma A P) =>
sigma_comm A P (fun (_ : sigma A P) => sigma A P) (pair A P) (fun (_ : sigma A P) (_ : sigma A P) => sigma A P) (fun (x : sigma A P) (_ : sigma A P) => x) u
:: sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u.
Rewrite sigma_beta.
Definition fst :=
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim A P u (fun (_ : sigma A P) => A) (fun (a : A) (_ : P a) => a).
Definition snd :=
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim
A P u
(fun (u : sigma A P) => P (fst A P u))
(fun (a : A) (b : P a) => b).
Definition contrR_true := sigmaR bool (fun (b : bool) => b = true).
Definition contrR_false := sigmaR bool (fun (b : bool) => b = false).
Definition contrR_true_inhab : contrR_true := ({ fst = true ; snd = (idpath true :: fst = true) } :: { fst : bool ; snd : fst = true }).
Definition contrR_false_inhab : contrR_false := ({ fst = false ; snd = (idpath false :: fst = false) } :: { fst : bool ; snd : fst = false }).
Parameter reflectR : contrR_true == contrR_false.
Definition fooR : true = true := (contrR_true_inhab.snd :: contrR_true_inhab.fst = true).
Definition barR : true = false := ((rewrite reflectR in (contrR_true_inhab :: contrR_false)).snd :: contrR_true_inhab.fst = false). (* succeeds *)
Definition contr_true := sigma bool (fun (b : bool) => b = true).
Definition contr_false := sigma bool (fun (b : bool) => b = false).
Definition contr_true_inhab : contr_true := pair bool (fun (b : bool) => b = true) true (idpath true).
Definition contr_false_inhab : contr_false := pair bool (fun (b : bool) => b = false) false (idpath false).
Parameter reflect : contr_true == contr_false.
Definition foo : true = true := (snd bool (fun (b : bool) => b = true) contr_true_inhab :: fst bool (fun (b : bool) => b = true) contr_true_inhab = true).
Definition bar : true = false := (snd bool (fun (b : bool) => b = false) (rewrite reflect in (contr_true_inhab :: contr_false)) :: fst bool (fun (b : bool) => b = false) (rewrite reflect in contr_true_inhab :: contr_false) = false). (* errors with
Typing error: sig.br:122:34: expression
snd bool (fun (b : bool) => b = false)
(rewrite reflect in contr_true_inhab) has type
fst bool (fun (b : bool) => b = false)
(rewrite reflect in contr_true_inhab)
=
false but should have type true = false
*)This comes from a discussion on the HoTT mailing list.
We only have the weak head normalization whnf e, but it would probably be useful to have other kinds of normalization, maybe strong normalization, or even something more custom-style.
We rely on uniqueness of typing in many places, I think. It says that if e has types A and B then A = B. However, it seems to me that we are breaking uniqueness with the kind of record types we implemented. Consider:
Parameter A : Type.
Parameter B : A -> Type.
Parameter a : A.
Parameter b : B a.
Then the record
{ x = a ; y = b }
has types {x : A ; y : B a} as well as {x : A ; y : B x}, and these do not seem to be equal. What to do? Uniqueness of typing seems like a nice property to have.
When using hint p to solve x :: B where the inferred type of x is A, there is a 3x3 grid of possible uses:
rewrite using \ use p to rewrite in: | A | B | A and B
-------------------------------------|---------|---------|---------
p | | |
-------------------------------------|---------|---------|---------
sym p | | |
-------------------------------------|---------|---------|---------
p and sym p | | |
Am I correct that equation is the bottom right corner, and rewrite is the bottom left corner?
It would be nice to be able to pick any square of this matrix, when I want to avoid loops, and also for debugging purposes. I propose using rewrite_inside/rewrite, rewrite_outside, and rewrite_both/equation for the first, second, and third columns, and being able to append ->, <-, and <-> for the first, second, and third rows, with the third row being the default. (But the syntax doesn't matter that much.)
What is the syntax of J? brazil.pdf says J_{T} ([x y p . U], [z . e1], e2, {e3}, {e4}) (where curlies here are pink in the pdf), but the Brazilians disagree:
Definition Type := Universe f0.
Definition transport :=
fun (A : Type)
(P : A -> Type)
(x y : A)
(p : x = y)
(z : forall x : A, P x) =>
J ([x y p. P x], [x . z x], p) :: P y.gives
Warning: Why are terms y = x and A equal?
Typing error: examples/interval.br:9:18: expression p has type y = x
but should have type A
Using J ([p x y. P x], [x . z x], p) :: P y instead gives the extremely confusing
Typing error: examples/interval.br:9:27: expression z x has type P x
but should have type x x
Using J ([p0 k0 k1. P k0], [k . z k], p) :: P y gives the less confusing but still ill-typed
Typing error: examples/interval.br:9:31: expression z k has type P k
but should have type x k
Where is it pulling the x from? Further testing suggests that the error message is broken, as it cares about argument order of the enclosing function...maybe there's a deBruijn indexing bug?
Definition transport :=
fun (A : Type)
(P : A -> Type)
(_ y : A)
(p : y = y)
(z : forall x : A, P x) =>
J ([p0 k0 k1. P k0], [k . z k], p) :: P y.gives
Typing error: examples/interval.br:9:31: expression z k has type P k
but should have type _ k
while
Definition transport :=
fun (A : Type)
(P : A -> Type)
(x y : A)
(p : y = y)
(z : forall x : A, P x) =>
J ([p0 k0 k1. P k0], [k . z k], p) :: P y.
gives
Typing error: examples/interval.br:9:31: expression z k has type P k
but should have type x k
Also, the "syntax error" messages would be more helpful if they said what characters they expected.
For instance:
Parameter t : assume A : Type in A.
Check t.
prints
⊢ t : A₀
See https://travis-ci.org/JasonGross/tt/builds/27975533. (Tangentially, @andrejbauer, have you enabled Travis for andrejbauer/tt?)
The programming language has no data structures, which makes it hard to program any sort of interesting algorithm. I am hesitant to have a large-scale language on top of type theory (i.e., a whole new level of simple types), but maybe that is what we need. We could first experiment with an untyped language that has good support for the common structures (lists, dictionaries).
I tried to prove sigma_eta', and got this error on the following code:
Definition Type := Universe f0.
Parameter sigma : forall (A : Type), (A -> Type) -> Type.
Parameter pair :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a),
sigma A P.
Parameter sigma_elim :
forall (A : Type)
(P : A -> Type)
(u : sigma A P)
(C : sigma A P -> Type),
(forall (a : A) (b : P a), C (pair A P a b)) -> C u.
Parameter sigma_beta :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a)
(C : sigma A P -> Type)
(f : forall (a : A) (b : P a), C (pair A P a b)),
sigma_elim A P (pair A P a b) C f == f a b.
Parameter sigma_eta :
forall (A : Type)
(P : A -> Type)
(u : sigma A P),
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u.
Rewrite sigma_beta.
Definition fst :=
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim A P u (fun (_ : sigma A P) => A) (fun (a : A) (_ : P a) => a).
Definition snd :=
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim
A P u
(fun (u : sigma A P) => P (fst A P u))
(fun (a : A) (b : P a) => b).
Parameter X : Type.
Parameter Q : X -> Type.
Parameter x : X.
Parameter y : Q x.
Definition check_fst :=
refl x :: x == fst X Q (pair X Q x y).
Definition check_snd :=
refl y :: y == snd X Q (pair X Q x y).
Parameter R : sigma X Q -> Type.
Parameter z : R (pair X Q x y).
Definition check_fst_fst :=
refl x ::
fst X Q
(fst (sigma X Q) R
(pair (sigma X Q) R (pair X Q x y) z)
)
== x.
Definition check_snd_fst :=
refl y ::
snd X Q
(fst (sigma X Q) R
(pair (sigma X Q) R (pair X Q x y) z)
)
== y.
Definition check_snd_snd :=
refl z ::
snd (sigma X Q) R
(pair (sigma X Q) R (pair X Q x y) z)
== z.
Definition sigma_eta' :=
fun
(A : Type)
(P : A -> Type)
(u v : sigma A P)
(e1 : fst A P u == fst A P v) =>
equation e1 in
fun (e2 : snd A P u == snd A P v) =>
equation sigma_eta A P u in
((refl u
:: sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
== sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b))
:: u == v).In a structure (formerly known as module or record) we have the following problem. Consider:
Axiom A : Type.
Axiom a : A.
Let cow := { horn as x := a, tail := (refl a :: x == x) }.
Check cow.
The output is:
A is assumed.
a is assumed.
cow is defined.
⊢ {horn as x := a, tail as tail := (refl a)}
: {horn as x : A, tail as tail : (a ≡ a)}
The type of cow is wrong, it should be {horn as x : A, tail as tail : (x ≡ x)}. The problem is that currently when the tail field is evaluated x is bound to a : A. Instead, it should be bound to x : A and we should have a beta hint x == a. This is what @SkySkimmer was talking about in #63
The programming language needs destructors, i.e. some sort of match statements that will let us inspect judgements. Implementing such destructors will also lead to the question on how to implement patterns.
Vladimir has the following computation rule for strict equality J:
J(T, [x y p . P], [z . e], a, a, refl) == e[a/z]
Why not the following:
J(T, [x y p . P], [z . e], a, b, p) == e[a/z]
This says in a strong way that strict equality types are proof irrelevant.
Currently the record types are implemented so that they may contain any number of fields:
{ lbl1 : type1 ; ... ; lblN : typeN }
This is convenient for the user, but it makes the code hairy. Also, it's going to make record types hard to work with on the meta-level in tt. Here is another possibility: we define a primitive dependent sum which has just two fields with fixed names fst and snd:
{ fst : type1 ; snd : type2 }
(of course type2 depends on type1) We then provide sufficient sugar for the general records (as above) to be implemented as nested dependent sums. We would still have labels and all that, so to the user it would all look like it does now. But in addition any theorem stated about dependent sum would apply to any record type.
One drawback is that we would need to treat records with a single field differently.
I wonder how hard it would be to do this. Essentially we need to map teh labels lblN to suitable combinations of projections snd.snd. ....snd.fst.
I am not sure whether this will be needed, but in general we would want to have parallel substitution of variables, e.g.,
e where x := e1 and y := e2 and z := e3
It may be better to wait with this until the programming language supports dictionaries or some such, because then we could write
e where <dict>
and e where x := e1 and y := e2 and z := e3 is just sugar for
e where { x : e1, y : e2, z : e3 }
Also, could dictionaries at the level of programming language be the same thing as records in type theory? Or to be more specific, the canonical elements of a record type would correspond to dictionaries.
At the moment a vertex is a product, which makes it hard to remember which component is the out-edges and which the in-edges. It would be better to have a record type with named files. And while at it, the code in Context can use more comments, too.
Brazil seems to be failing to notice that (fst A P (pair A P a b)) and a are the same. I suspect it has something to do with being under binders, but this is just a guess.
Definition Type := Universe f0.
Parameter sigma : forall (A : Type), (A -> Type) -> Type.
Parameter pair :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a),
sigma A P.
Parameter sigma_elim :
forall (A : Type)
(P : A -> Type)
(u : sigma A P)
(C : sigma A P -> Type),
(forall (a : A) (b : P a), C (pair A P a b)) -> C u.
Parameter sigma_beta :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a)
(C : sigma A P -> Type)
(f : forall (a : A) (b : P a), C (pair A P a b)),
sigma_elim A P (pair A P a b) C f == f a b.
Parameter sigma_comm :
forall (A : Type)
(P : A -> Type)
(Q : sigma A P -> Type)
(q : forall (x : A) (p : P x), Q (pair A P x p))
(R : forall (x : sigma A P), Q x -> Type)
(f : forall (x : sigma A P) (q : Q x), R x q)
(u : sigma A P),
rewrite sigma_beta in
sigma_elim A P u
(fun (x : sigma A P) => R x (sigma_elim A P x Q (fun (x : A) (p : P x) => q x p)))
(fun (x : A) (p : P x) => f (pair A P x p) (q x p) :: R (pair A P x p) (sigma_elim A P (pair A P x p) Q q))
==
f u (sigma_elim A P u Q q).
Definition sigma_half_eta :=
fun (A : Type)
(P : A -> Type)
(u : sigma A P) =>
sigma_comm A P (fun (_ : sigma A P) => sigma A P) (pair A P) (fun (_ : sigma A P) (_ : sigma A P) => sigma A P) (fun (x : sigma A P) (_ : sigma A P) => x) u
:: sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u.
Rewrite sigma_beta.
Definition fst :=
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim A P u (fun (_ : sigma A P) => A) (fun (a : A) (_ : P a) => a).
Definition snd :=
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim
A P u
(fun (u : sigma A P) => P (fst A P u))
(fun (a : A) (b : P a) => b).
(*match u as u' with (a; b) => (fun u p => (fst p; snd p)) (a; b) end == match u with (a; b) => (a; b) end
match u as u' with (a; b) => (fun u p => (fst p; snd p)) (a; b) end == match u with (a; b) => (a; b) end
(fun u p => (fst p; snd p)) u ... == match u with (a; b) => (a; b) end
(fst u; snd u) == (fun u p => p) u (match u with (a; b) => (a; b) end)
(fst u; snd u) == match u with (a; b) => (a; b) end
(fst u; snd u) == u*)
Definition sigma_eta :=
fun (A : Type)
(P : A -> Type)
(u : sigma A P)
=>
((*rewrite sigma_comm A P (fun (_ : sigma A P) => sigma A P) (pair A P) (fun (_ : sigma A P) (_ : sigma A P) => sigma A P) (fun (_ : sigma A P) (x : sigma A P) => pair A P (fst A P x) (snd A P x)) u in*)
(((rewrite sigma_half_eta A P u in
refl u
:: sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P a b)
== u) (* match u with (a; b) => (a; b) end == u *)
:: sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P (fst A P (pair A P a b)) (snd A P (pair A P a b)))
== u) (* match u with (a; b) => (fst (a; b); snd (a; b)) end == u *))). (* ((
:: sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => (fun (u : sigma A P) (p : sigma A P) => pair A P (fst A P p) (snd A P p)) (pair A P a b) (pair A P a b))
== u) (* match u with (a; b) => (fun u p => (fst p; snd p)) (a; b) (a; b) end == u *)
:: (fun (u : sigma A P) (p : sigma A P) => pair A P (fst A P p) (snd A P p)) u (sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P a b))
== u) (* (fun u p => (fst p; snd p)) u (match u with (a; b) => (a; b) end) == u *)
:: pair A P (fst A P u) (snd A P u)
== u.*)
(* Warning: Why are terms
u
and
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) =>
pair A P (fst A P (pair A P a b))
(snd A P (pair A P a b)))
equal?
Warning: Why are terms
u
and
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) =>
pair A P (fst A P (pair A P a b))
(snd A P (pair A P a b)))
equal?
Typing error: examples/sigma.br:81:9: expression refl u has type
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u
but should have type sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) =>
pair A P (fst A P (pair A P a b))
(snd A P (pair A P a b)))
==
u *)There is a bug that inverts the order of arguments of functions. Writing [fun (x y : A) => something] is getting interpreted as [fun y : A => fun x : A => something] instead of [fun x : A => fun y : A => something]. The bug might be hidden somewhere in the parser or the conversion to de Bruijn indices.
This bug was not easy to find, because I was testing the program with the church numerals example posted on the blog. The functions defined there were not affected by this bug, because [plus] and [times] are commutative. The [power] function is defined in the wrong order in the example (it should be [fun n => fun m => m n] instead of [fun n => fun m => n m]), but this "double inversion" makes it calculate the correct result!
Definition Type := Universe f0.
Parameter bool : Type.
Parameter true false : bool.
Parameter bool_ind :
forall (P : bool -> Type) (b : bool), P true -> P false -> P b.
Parameter bool_ind_false :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P false x y == y.
Parameter bool_ind_true :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P true x y == x.
Rewrite bool_ind_true.
Rewrite bool_ind_false.
Definition cond := fun (A : Type) => bool_ind (fun (C : bool) => A).
Definition cond_false :=
fun (A : Type) (x : A) (y : A) =>
(refl y :: bool_ind (fun U : bool => A) false x y == y).
Definition cond_true :=
fun (A : Type) (x : A) (y : A) =>
(refl x :: bool_ind (fun V : bool => A) true x y == x).
Definition or := fun (a b : bool) => cond bool a true b.
Definition and := fun (a b : bool) => cond bool a b false.
Definition sigma := fun (A : Type) (P : A -> Type) => { fst : A ; snd : P fst }.
Definition pair := fun (A : Type) (P : A -> Type) (x : A) (p : P x)
=> { fst = x ; snd = (p :: P fst) } :: sigma A P.
Definition contr_true := sigma bool (fun (b : bool) => b = true).
Definition contr_false := sigma bool (fun (b : bool) => b = false).
Definition contr_true_inhab : contr_true := ({ fst = true ; snd = (idpath true :: fst = true) } :: { fst : bool ; snd : fst = true }).
Definition contr_false_inhab : contr_false := ({ fst = false ; snd = (idpath false :: fst = false) } :: { fst : bool ; snd : fst = false }).
Parameter reflect : contr_true == contr_false.
Definition foo : true = true := (contr_true_inhab.snd :: contr_true_inhab.fst = true)gives
Warning: <<1142>>Why are terms idpath true and true equal?
Typing error: sig.br:43:34: expression contr_true_inhab.snd has type
(fun (b : bool) => b = true) contr_true_inhab.snd
but should have type contr_true_inhab.fst = true
I'm very suspicious of contr_true_inhab.snd showing up in its own type.
It would be nice to be able to ask brazilians to ship back a transcript of their hint usage: for each goal that needs rewriting hints, a list of the hints used, and the final things that it had to unify. Something between -V 2 and -V 3. I'm ok with this being a whole-file or command line option, but it would be nicer to have an equation_debug and rewrite_debug and a Set Debug Hints. or something.
Definition ∑ := fun (A : Universe f0) (P : A -> Universe f0) => { 1 : A ; 2 : P 1 }.Syntax error: sig.br:1:12: Unexpected character \226
Chris asks whether Brazilian type theory has an eliminator for Id type. I think so, at least in the orthodox formulation. In the bidirectional version with handlers it might go away.
Just like we have a separation between Tt.term and Tt.ty we should have a separation between terms that may contain de Bruijn indices (bare bound variables) and those that do not. This is likely going to prevent the sort of headaches we experience now when we forget to use Tt.abstract or Tt.unabstract.
I think I found some code where I can manually cast across a judgmental equality, but Brazilians don't notice that my Rewrite hint applies, and if I try to tell them more forcefully (by filling in the arguments), they run around in loops. But I can coerce manually. Except that when I try to declare it as a hint, then the brazil starts looping.
Definition Type := Universe f0.
Definition Type1 := Universe f1.
(** Symmetry of equality *)
Definition sym : forall (A : Type) (a b : A), a == b -> b == a :=
fun (A : Type) (a b : A) (p : a == b) => equation p in (refl a :: b == a).
(** Transitivity of equality *)
Definition trans :=
fun (A : Type) (a b c : A) (p : a == b) (q : b == c) =>
equation p in
equation q in (refl b :: a == c).
Definition cast :=
fun (A B : Type1) (p : A == B) (x : A) => equation p in (x :: B).
Definition str_apD10 := fun (A : Type1) (P : A -> Universe f2) (f g : forall x : A, P x) (x : A) (H : f == g) => equation H in (refl (f x) :: f x == g x).
Definition str_apD := fun (A : Type1) (P : A -> Universe f2) (f : forall x : A, P x) (x y : A) (H : x == y) => equation H in (refl (f x) :: f x == f y).
(* sigmas *)
Parameter sigT : forall (A : Type1) (P : A -> Type1), Type1.
Parameter existT : forall (A : Type1) (P : A -> Type1) (x : A) (H : P x), sigT A P.
Parameter pr1 : forall (A : Type1) (P : A -> Type1), sigT A P -> A.
Parameter pr2 : forall (A : Type1) (P : A -> Type1) (x : sigT A P), P (pr1 A P x).
Parameter sigT_beta_pr1 : forall (A : Type1) (P : A -> Type1) (x : A) (H : P x), pr1 A P (existT A P x H) == x.
Rewrite sigT_beta_pr1.
Parameter sigT_beta_pr2 : forall (A : Type1) (P : A -> Type1) (x : A) (H : P x), pr2 A P (existT A P x H) == H.
Rewrite sigT_beta_pr2.
Parameter sigT_eta : forall (A : Type1) (P : A -> Type1) (x : sigT A P), existT A P (pr1 A P x) (pr2 A P x) == x.
Rewrite sigT_eta.
(*********)
(* prods *)
Parameter prod : Type -> Type -> Type.
Parameter pair : forall (A B : Type) (x : A) (y : B), prod A B.
Parameter fst : forall (A B : Type), prod A B -> A.
Parameter snd : forall (A B : Type), prod A B -> B.
Parameter prod_beta_fst : forall (A B : Type) (x : A) (y : B), fst A B (pair A B x y) == x.
Rewrite prod_beta_fst.
Parameter prod_beta_snd : forall (A B : Type) (x : A) (y : B), snd A B (pair A B x y) == y.
Rewrite prod_beta_snd.
Parameter prod_eta : forall (A B : Type) (x : prod A B), pair A B (fst A B x) (snd A B x) == x.
Rewrite prod_eta.
(*********)
(* lists *)
Parameter list : Type -> Type.
Parameter nil : forall T : Type, list T.
Parameter cons : forall (T : Type) (x : T) (xs : list T), list T.
Parameter list_ind :
forall (T : Type) (P : list T -> Type) (IHnil : P (nil T)) (IHcons : forall (x : T) (xs : list T), P xs -> P (cons T x xs)) (ls : list T),
P ls.
Parameter list_ind_nil :
forall (T : Type) (P : list T -> Type) (IHnil : P (nil T)) (IHcons : forall (x : T) (xs : list T), P xs -> P (cons T x xs)),
list_ind T P IHnil IHcons (nil T) == IHnil.
Parameter list_ind_cons :
forall (T : Type) (P : list T -> Type) (IHnil : P (nil T)) (IHcons : forall (x : T) (xs : list T), P xs -> P (cons T x xs)) (x : T) (xs : list T),
list_ind T P IHnil IHcons (cons T x xs) == IHcons x xs (list_ind T P IHnil IHcons xs).
Rewrite list_ind_nil.
Rewrite list_ind_cons.
(**********************)
(* booleans *)
Parameter bool : Type.
Parameter true false : bool.
Parameter bool_ind :
forall (P : bool -> Type) (b : bool), P true -> P false -> P b.
Parameter bool_ind_false :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P false x y == y.
Parameter bool_ind_true :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P true x y == x.
Definition cond := fun (A : Type) => bool_ind (fun (_ : bool) => A).
Rewrite bool_ind_false.
Rewrite bool_ind_true.
Definition cond_true :=
fun (A : Type) (x : A) (y : A) =>
(refl x :: bool_ind (fun _ : bool => A) true x y == x).
Definition cond_false :=
fun (A : Type) (x : A) (y : A) =>
rewrite bool_ind_false in
(refl y :: bool_ind (fun _ : bool => A) false x y == y).
Definition or := fun (a b : bool) => cond bool a true b.
Definition and := fun (a b : bool) => cond bool a b false.
Definition bool_test1 :=
fun (A : Type) (a b : A) =>
(refl a :: (a == cond A (or false true) a b)).
(********************************)
(* sums *)
Parameter sum : Type -> Type -> Type.
Parameter inl : forall (A B : Type), A -> sum A B.
Parameter inr : forall (A B : Type), B -> sum A B.
Parameter sum_ind :
forall (A B : Type) (P : sum A B -> Type), (forall (x : A), P (inl A B x)) -> (forall (x : B), P (inr A B x)) -> forall b : sum A B, P b.
Parameter sum_ind_inl :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : A),
sum_ind A B P IHinl IHinr (inl A B x) == (IHinl x).
Parameter sum_ind_inr :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : B),
sum_ind A B P IHinl IHinr (inr A B x) == (IHinr x).
Rewrite sum_ind_inl.
Rewrite sum_ind_inr.
Parameter sum_match_commutes :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (C : forall (x : sum A B), P x -> Type)
(f : forall (x : sum A B) (p : P x), C x p)
(x : sum A B),
sum_ind A B (fun x : sum A B => C x (sum_ind A B P IHinl IHinr x))
(fun (x : A) => equation sum_ind_inl in
(f (inl A B x) (IHinl x) :: C (inl A B x) (sum_ind A B P IHinl IHinr (inl A B x))))
(fun (x : B) => equation sum_ind_inr in
(f (inr A B x) (IHinr x) :: C (inr A B x) (sum_ind A B P IHinl IHinr (inr A B x))))
x
== f x (sum_ind A B P IHinl IHinr x).
Definition sum_half_eta :=
fun (A B : Type) (x : sum A B) =>
sum_match_commutes A B (fun (x : sum A B) => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) (fun (x : sum A B) (_ : sum A B) => sum A B) (fun (x : sum A B) (_ : sum A B) => x) x
:: sum_ind A B (fun _ : sum A B => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) x == x.
Rewrite sum_half_eta.
(*********)
Parameter A B C : Type.
Parameter f : A -> B.
Parameter g : A -> C.
Parameter a : unit -> A.
(*(* we track f, g, a as the things we can inspect *)
Definition allowable_next_step_type := prod bool (prod bool bool).
Definition initial_allowable_steps : allowable_next_step_type := pair bool (prod bool bool) true (pair bool bool true true).*)
Definition hint_dummy_result := unit.
Definition unsolved_term_hint_type := fun (goal : Type) => Type.
Parameter solved_term_hint_type : Type -> Type1. (* := fun (goal : Type) => Type. *)
Parameter can_solve : unsolved_term_hint_type == solved_term_hint_type. (* so we can use this as a hint and not need to worry about whnf doing it for us *)
Definition start_auto : forall (goal : Type), unsolved_term_hint_type goal := fun (goal : Type) => unit.
Parameter hint_progress :
forall (result : sigT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))),
unsolved_term_hint_type (pr1 Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
result).
Parameter hint_finished :
forall (result : sigT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))),
solved_term_hint_type (pr1 Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
result).
Parameter start_auto_by_fiat : forall (goal : Type), start_auto goal
== hint_progress (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
goal
(fun x : goal => x))).
Rewrite start_auto_by_fiat.
Parameter solve_by_auto_or_block : forall (goal : Type) (auto_result : solved_term_hint_type goal), goal.
Parameter finish_auto_by_fiat : forall (goal : Type) (term : unit -> goal),
solve_by_auto_or_block goal
(* bug that I can't rewrite? *)
((cast
(solved_term_hint_type
(pr1 Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
(existT Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
goal
(existT Type
(fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit term))))
(solved_term_hint_type goal)
(str_apD Type (fun _ : Type => Type1) solved_term_hint_type
(pr1 Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
(existT Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
goal
(existT Type
(fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit term)))
goal
(sigT_beta_pr1 Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit
term)))
((hint_finished (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit
term)))
)))
== term ().
Rewrite finish_auto_by_fiat.
Definition declare_hint := fun (T1 : Type) (T2 : Type) (transformer : T1 -> T2) =>
forall (goal : Type) (term : T2 -> goal),
hint_progress (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
T2
term))
==
hint_progress (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
T1
(fun x : T1 => term (transformer x)))).
Parameter step_auto_f : declare_hint A B f.
Parameter step_auto_g : declare_hint A C g.
Parameter step_auto_a : declare_hint unit A a.
Parameter prefinish_auto_by_fiat : forall (goal : Type) (term : unit -> goal),
(equation (str_apD10 Type (fun _ : Type => Type1) unsolved_term_hint_type solved_term_hint_type goal can_solve) in
(((hint_progress (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit
term)))
:: unsolved_term_hint_type goal)
:: solved_term_hint_type goal))
==
(* bug that I can't rewrite? *)
((cast
(solved_term_hint_type
(pr1 Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
(existT Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
goal
(existT Type
(fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit term))))
(solved_term_hint_type goal)
(str_apD Type (fun _ : Type => Type1) solved_term_hint_type
(pr1 Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
(existT Type
(fun (goal0 : Type) =>
sigT Type
(fun (hypotheses : Type) =>
coerce (f1,
hypotheses -> goal0)))
goal
(existT Type
(fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit term)))
goal
(sigT_beta_pr1 Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit
term)))
((hint_finished (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit
term)))))
:: solved_term_hint_type goal).
(* If I uncomment out this line native brazilians loop at the end, or at least, run for a while on high cpu (bytecode brazilians do, too) *)
(* Rewrite prefinish_auto_by_fiat. *)We need a name for the programming language that the kernel evaluates. Maybe something related to travelling to the Andromeda galaxy, or something from Greek mythology?
Why does this hint, which exactly matches the goal (up to symmetry), not get used?
Definition Type := Universe f0.
Parameter sigma : forall (A : Type), (A -> Type) -> Type.
Parameter pair :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a),
sigma A P.
Parameter sigma_elim :
forall (A : Type)
(P : A -> Type)
(u : sigma A P)
(C : sigma A P -> Type),
(forall (a : A) (b : P a), C (pair A P a b)) -> C u.
Parameter sigma_half_eta' :
forall (A : Type)
(P : A -> Type)
(u : sigma A P),
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u.
Definition sigma_eta_helper_helper' :=
fun (A : Type)
(P : A -> Type)
(u : sigma A P)
=>
rewrite sigma_half_eta' A P u in
refl u
:: sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P a b)
== u (* match u with (a; b) => (a; b) end == u *).
(* Warning: Why are terms
u
and
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
equal?
Typing error: examples/sigma.br:34:5: expression refl u has type u == u
but should have type sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u *)Definition Type := Universe f0.
Definition sym := fun (A : Type) (x y : A) (p : x == y) => rewrite p in (refl x :: y == x).
Parameter sigma : forall (A : Type), (A -> Type) -> Type.
Parameter pair :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a),
sigma A P.
Parameter sigma_elim :
forall (A : Type)
(P : A -> Type)
(u : sigma A P)
(C : sigma A P -> Type),
(forall (a : A) (b : P a), C (pair A P a b)) -> C u.
Parameter sigma_beta :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a)
(C : sigma A P -> Type)
(f : forall (a : A) (b : P a), C (pair A P a b)),
sigma_elim A P (pair A P a b) C f == f a b.
Parameter sigma_eta :
forall (A : Type)
(P : A -> Type)
(u : sigma A P),
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u.
Parameter sigma_comm :
rewrite sigma_beta in
forall (A : Type)
(P : A -> Type)
(Q : sigma A P -> Type)
(q : forall (x : A) (p : P x), Q (pair A P x p))
(R : forall (x : sigma A P), Q x -> Type)
(f : forall (x : sigma A P) (q : Q x), R x q)
(u : sigma A P),
f u (sigma_elim A P u Q q)
==
sigma_elim A P u
(fun (x : sigma A P) => R x (sigma_elim A P x Q (fun (x : A) (p : P x) => q x p)))
(fun (x : A) (p : P x) => f (pair A P x p) (q x p) :: R (pair A P x p) (sigma_elim A P (pair A P x p) Q q)).
Definition sigma_eta_sym :=
fun (A : Type)
(P : A -> Type)
(u : sigma A P) =>
sym (sigma A P)
(sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b))
u
(sigma_eta A P u).
Definition fst :=
rewrite sigma_beta in
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim A P u (fun (_ : sigma A P) => A) (fun (a : A) (_ : P a) => a).
Definition snd :=
rewrite sigma_beta in
fun (A : Type) (P : A -> Type) (u : sigma A P) =>
sigma_elim
A P u
(fun (u : sigma A P) => P (fst A P u))
(fun (a : A) (b : P a) => b).
Definition sigma_eta' :=
fun
(A : Type)
(P : A -> Type)
(u : sigma A P) =>
rewrite sigma_beta in
rewrite sigma_comm in
(refl (pair A P (fst A P u) (snd A P u))
:: pair A P (fst A P u) (snd A P u)
== pair A P (fst A P (sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)))
(snd A P (sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)))).File brazilmacros.tex seems to be missing for generating paris/slides.tex
If I don't fill in the arguments to sigma_eta in the following, the term doesn't typecheck:
Definition Type := Universe f0.
Parameter sigma : forall (A : Type), (A -> Type) -> Type.
Parameter pair :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a),
sigma A P.
Parameter sigma_elim :
forall (A : Type)
(P : A -> Type)
(u : sigma A P)
(C : sigma A P -> Type),
(forall (a : A) (b : P a), C (pair A P a b)) -> C u.
Parameter sigma_beta :
forall (A : Type)
(P : A -> Type)
(a : A)
(b : P a)
(C : sigma A P -> Type)
(f : forall (a : A) (b : P a), C (pair A P a b)),
sigma_elim A P (pair A P a b) C f == f a b.
Parameter sigma_eta :
forall (A : Type)
(P : A -> Type)
(u : sigma A P),
sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
(fun (a : A) (b : P a) => pair A P a b)
==
u.
Definition sigma_comm :=
fun (A : Type)
(P : A -> Type)
(Q : sigma A P -> Type)
(q : forall (x : A) (p : P x), Q (pair A P x p))
(R : forall (x : sigma A P), Q x -> Type)
(f : forall (x : sigma A P) (q : Q x), R x q)
(u : sigma A P) =>
rewrite sigma_eta A P u in
f (sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P a b))
(sigma_elim A P (sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P a b))
Q q)
:: R u (sigma_elim A P u Q q).Rewriting seems to be a mess. We should fix it so that it is more predictable and not terribly expensive. I would like to limit allowable rewrites as follows. First, every rewrite rule is of the form
f P1 ... Pn = t
where Pi are patterns. We say that the above rule is associated with f and that its arity is n. We may require that all active rules associated with f have the same arity. The idea is that, in order to figure out whether a rewrite rule applies, we just look at the head of the spine f and see if there's a rewrite rule of correct arity associated with it.
We also need a mechanism for explaining which arguments in a spine
f e1 ... en
should be put in whnf before we try to match the spine against a pattern. Probably we could use an annotation. For instance, consider the definition of natural numbers:
Parameter N : Type.
Parameter 0 : N.
Parameter S : N -> N.
Parameter N_ind :
forall (P : N -> Type),
P 0 ->
(forall n : N, P n -> P (S n)) ->
forall (m : N), P m.
Parameter N_ind_0 :
forall
(P : N -> Type)
(z : P 0)
(f : forall n : N, P n -> P (S n)),
N_ind P z f 0 == z.
Parameter N_ind_S :
forall
(P : N -> Type)
(z : P 0)
(f : forall n : N, P n -> P (S n))
(m : N),
N_ind P z f (S m) == f m (N_ind P z f m).
Here we would like to associate two rewrite rules with N_ind (corresponding to N_ind_0 and N_ind_S):
N_ind ?P ?z ?f 0 = ?z
N_ind ?P ?z ?f (S ?m) = f ?n (N_ind ?P ?z ?f ?m)
Both rewrite rules have arity 4. Furthermore, we should somehow indicate that the fourth argument of N_ind should be put in whnf before matching, but not the others. So maybe something like this could be written:
rewrite N_ind _ _ _ * using [N_ind_0, N_ind_S] in ....
The * indicates the arguments which should undergo weak-head normalization before the match.
This scheme seems to be somewhat efficient: given a spine
f e1 e2 ... en
we can find rewrite rules associated with f whose arity is less or equal n. Then we weak-head normalize those arguments ei which should be normalized according to the rewrite rules for f, and we try to match them.
I think we cover most cases this way. What do you think?
I've nearly managed to implement a non-backtracking auto "tactic", I think (right now it only allows hints with a single hypothesis to solve). The problem is that it's non-informative; the only way I can convince the Brazilians to run my tactic is by telling them what it will eventually output. (And then they happily run it, as far as I can tell, ignoring what I gave them except as a way to notice that they're done.) Alternatively, if I tell them to throw away the term they build after building it, they will also happily build me my term (I think). The block I'm running into, I think, is that I can only rewrite at one level at a time; I can't moving things from the type level into the term level in the middle of rewriting.
This also means I can't effectively debug it; I can't figure out why equation makes it work when I think it shouldn't work at all, while rewrite (in either direction) makes brazil run out of memory. What's the difference between rewrite and equation?
Anyway, if you're interested, here's the code:
Definition Type := Universe f0.
Definition Type1 := Universe f1.
(** Symmetry of equality *)
Definition sym : forall (A : Type) (a b : A), a == b -> b == a :=
fun (A : Type) (a b : A) (p : a == b) => equation p in (refl a :: b == a).
(** Transitivity of equality *)
Definition trans :=
fun (A : Type) (a b c : A) (p : a == b) (q : b == c) =>
equation p in
equation q in (refl b :: a == c).
Definition cast :=
fun (A B : Type1) (p : A == B) (x : A) => equation p in (x :: B).
Definition str_apD10 := fun (A : Type1) (P : A -> Universe f2) (f g : forall x : A, P x) (x : A) (H : f == g) => equation H in (refl (f x) :: f x == g x).
Definition str_apD := fun (A : Type1) (P : A -> Universe f2) (f : forall x : A, P x) (x y : A) (H : x == y) => equation H in (refl (f x) :: f x == f y).
(* sigmas *)
Parameter sigT : forall (A : Type1) (P : A -> Type1), Type1.
Parameter existT : forall (A : Type1) (P : A -> Type1) (x : A) (H : P x), sigT A P.
Parameter pr1 : forall (A : Type1) (P : A -> Type1), sigT A P -> A.
Parameter pr2 : forall (A : Type1) (P : A -> Type1) (x : sigT A P), P (pr1 A P x).
Parameter sigT_beta_pr1 : forall (A : Type1) (P : A -> Type1) (x : A) (H : P x), pr1 A P (existT A P x H) == x.
Rewrite sigT_beta_pr1.
Parameter sigT_beta_pr2 : forall (A : Type1) (P : A -> Type1) (x : A) (H : P x), pr2 A P (existT A P x H) == H.
Rewrite sigT_beta_pr2.
Parameter sigT_eta : forall (A : Type1) (P : A -> Type1) (x : sigT A P), existT A P (pr1 A P x) (pr2 A P x) == x.
Rewrite sigT_eta.
(*********)
(* prods *)
Parameter prod : Type -> Type -> Type.
Parameter pair : forall (A B : Type) (x : A) (y : B), prod A B.
Parameter fst : forall (A B : Type), prod A B -> A.
Parameter snd : forall (A B : Type), prod A B -> B.
Parameter prod_beta_fst : forall (A B : Type) (x : A) (y : B), fst A B (pair A B x y) == x.
Rewrite prod_beta_fst.
Parameter prod_beta_snd : forall (A B : Type) (x : A) (y : B), snd A B (pair A B x y) == y.
Rewrite prod_beta_snd.
Parameter prod_eta : forall (A B : Type) (x : prod A B), pair A B (fst A B x) (snd A B x) == x.
Rewrite prod_eta.
(*********)
(* lists *)
Parameter list : Type -> Type.
Parameter nil : forall T : Type, list T.
Parameter cons : forall (T : Type) (x : T) (xs : list T), list T.
Parameter list_ind :
forall (T : Type) (P : list T -> Type) (IHnil : P (nil T)) (IHcons : forall (x : T) (xs : list T), P xs -> P (cons T x xs)) (ls : list T),
P ls.
Parameter list_ind_nil :
forall (T : Type) (P : list T -> Type) (IHnil : P (nil T)) (IHcons : forall (x : T) (xs : list T), P xs -> P (cons T x xs)),
list_ind T P IHnil IHcons (nil T) == IHnil.
Parameter list_ind_cons :
forall (T : Type) (P : list T -> Type) (IHnil : P (nil T)) (IHcons : forall (x : T) (xs : list T), P xs -> P (cons T x xs)) (x : T) (xs : list T),
list_ind T P IHnil IHcons (cons T x xs) == IHcons x xs (list_ind T P IHnil IHcons xs).
Rewrite list_ind_nil.
Rewrite list_ind_cons.
(**********************)
(* booleans *)
Parameter bool : Type.
Parameter true false : bool.
Parameter bool_ind :
forall (P : bool -> Type) (b : bool), P true -> P false -> P b.
Parameter bool_ind_false :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P false x y == y.
Parameter bool_ind_true :
forall (P : bool -> Type) (x : P true) (y : P false),
bool_ind P true x y == x.
Definition cond := fun (A : Type) => bool_ind (fun (_ : bool) => A).
Rewrite bool_ind_false.
Rewrite bool_ind_true.
Definition cond_true :=
fun (A : Type) (x : A) (y : A) =>
(refl x :: bool_ind (fun _ : bool => A) true x y == x).
Definition cond_false :=
fun (A : Type) (x : A) (y : A) =>
rewrite bool_ind_false in
(refl y :: bool_ind (fun _ : bool => A) false x y == y).
Definition or := fun (a b : bool) => cond bool a true b.
Definition and := fun (a b : bool) => cond bool a b false.
Definition bool_test1 :=
fun (A : Type) (a b : A) =>
(refl a :: (a == cond A (or false true) a b)).
(********************************)
(* sums *)
Parameter sum : Type -> Type -> Type.
Parameter inl : forall (A B : Type), A -> sum A B.
Parameter inr : forall (A B : Type), B -> sum A B.
Parameter sum_ind :
forall (A B : Type) (P : sum A B -> Type), (forall (x : A), P (inl A B x)) -> (forall (x : B), P (inr A B x)) -> forall b : sum A B, P b.
Parameter sum_ind_inl :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : A),
sum_ind A B P IHinl IHinr (inl A B x) == (IHinl x).
Parameter sum_ind_inr :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : B),
sum_ind A B P IHinl IHinr (inr A B x) == (IHinr x).
Rewrite sum_ind_inl.
Rewrite sum_ind_inr.
Parameter sum_match_commutes :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (C : forall (x : sum A B), P x -> Type)
(f : forall (x : sum A B) (p : P x), C x p)
(x : sum A B),
sum_ind A B (fun x : sum A B => C x (sum_ind A B P IHinl IHinr x))
(fun (x : A) => equation sum_ind_inl in
(f (inl A B x) (IHinl x) :: C (inl A B x) (sum_ind A B P IHinl IHinr (inl A B x))))
(fun (x : B) => equation sum_ind_inr in
(f (inr A B x) (IHinr x) :: C (inr A B x) (sum_ind A B P IHinl IHinr (inr A B x))))
x
== f x (sum_ind A B P IHinl IHinr x).
Definition sum_half_eta :=
fun (A B : Type) (x : sum A B) =>
sum_match_commutes A B (fun (x : sum A B) => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) (fun (x : sum A B) (_ : sum A B) => sum A B) (fun (x : sum A B) (_ : sum A B) => x) x
:: sum_ind A B (fun _ : sum A B => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) x == x.
Rewrite sum_half_eta.
(*********)
Parameter unit' : Type.
Parameter tt : unit'.
Definition unsolved_term_hint_type := fun (goal : Type) => Type.
Parameter solved_term_hint_type : Type -> Type1. (* := fun (goal : Type) => Type. *)
Parameter can_solve : unsolved_term_hint_type == solved_term_hint_type. (* so we can use this as a hint and not need to worry about whnf doing it for us *)
Parameter start_auto : forall (goal : Type), Type.
Parameter auto_seed : forall (goal : Type), start_auto goal.
Parameter hint_progress :
forall (result : sigT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))),
Type. (*
unsolved_term_hint_type (pr1 Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
result). *)
Parameter hint_finished :
forall (result : sigT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))),
Type. (*
solved_term_hint_type (pr1 Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
result). *)
Parameter start_auto_by_fiat : forall (goal : Type), start_auto goal
== hint_progress (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
goal
(fun x : goal => x))).
Rewrite start_auto_by_fiat.
Parameter Im_all_done_but_you_cant_get_me_unless_you_already_have_me : forall T : Type, T -> Type.
Parameter Im_all_done_but_you_lost_me : forall T : Type, Type.
(*Parameter solve_by_auto_or_block : forall (goal : Type) (auto_result : hint_finished goal), goal.*)
Parameter finish_auto_by_fiat1 : forall (goal : Type) (term : unit' -> goal),
((hint_finished (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit'
term)))
)
== Im_all_done_but_you_lost_me goal.
Parameter finish_auto_by_fiat2 : forall (goal : Type) (term : unit' -> goal),
((hint_finished (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
unit'
term)))
)
== Im_all_done_but_you_cant_get_me_unless_you_already_have_me goal (term tt).
Rewrite finish_auto_by_fiat1.
Rewrite finish_auto_by_fiat2.
Definition declare_hint := fun (T1 : Type) (T2 : Type) (transformer : T1 -> T2) =>
forall (goal : Type) (term : T2 -> goal),
hint_progress (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
T2
term))
==
hint_progress (existT Type (fun (goal : Type) =>
sigT Type (fun (hypotheses : Type) =>
coerce (f1, hypotheses -> goal)))
goal
(existT Type (fun (hypotheses : Type) => coerce (f1, hypotheses -> goal))
T1
(fun x : T1 => term (transformer x)))).
Parameter A B C : Type.
Parameter f : A -> B.
Parameter g : A -> C.
Parameter h : A -> B.
Parameter a : unit' -> A.
Parameter step_auto_f : declare_hint A B f.
Parameter step_auto_g : declare_hint A C g.
Parameter step_auto_a : declare_hint unit' A a.
(* this shouldn't work, but it does... But it OOMs if the equation becomes a rewrite... *)
Definition test_auto1 : B :=
(* rewrite step_auto_f in*)
(* rewrite step_auto_g in*)
(* rewrite step_auto_a in*)
(* BUG! shouldn't need the B here, I think *)
((equation start_auto_by_fiat B in
(auto_seed B :: start_auto B)) :: Im_all_done_but_you_lost_me B).
Definition test_auto2 : B :=
rewrite step_auto_f in
rewrite step_auto_g in
rewrite step_auto_a in
(* BUG! shouldn't need the B here, I think *)
equation start_auto_by_fiat B in
((auto_seed B :: start_auto B) :: Im_all_done_but_you_cant_get_me_unless_you_already_have_me B (h (a tt))).Equality checks always extend the input context (verify that this is the case!), so it is uneccessary to join the context output by Equal with the one we passed in. It looks like this happens in a number of places.
In the long run we might be thankful for having a separate datatype for normal forms. That would defend against a lot of possible bugs. I know it's annoying, but still, it's not a lot of work, it catches a lot of errors, and it eliminates a bunch of assert false.
I can't find a syntax for elimination of = and ==, so it's kind of hard to define the opposite of a path. What would be a good syntax (assuming there isn't one alredy)? Maybe just a primitive constant of a suitable type?
It seems there's too much controversy with calling it "Brazil". What would be a better name? I am thinking nothing is wrong with tt. Martin Escardo suggested Andromeda, which seems far enough (although we're on a collision course with it).
In case you're interested in where speed issues begin to crop up:
Definition Type := Universe f0.
(* sums *)
Parameter sum : Type -> Type -> Type.
Parameter inl : forall (A B : Type), A -> sum A B.
Parameter inr : forall (A B : Type), B -> sum A B.
Parameter sum_ind :
forall (A B : Type) (P : sum A B -> Type), (forall (x : A), P (inl A B x)) -> (forall (x : B), P (inr A B x)) -> forall b : sum A B, P b.
Parameter sum_ind_inl :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : A),
sum_ind A B P IHinl IHinr (inl A B x) == (IHinl x).
Parameter sum_ind_inr :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : B),
sum_ind A B P IHinl IHinr (inr A B x) == (IHinr x).
Rewrite sum_ind_inl.
Rewrite sum_ind_inr.
Parameter sum_match_commutes :
forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (C : forall (x : sum A B), P x -> Type)
(f : forall (x : sum A B) (p : P x), C x p)
(x : sum A B),
sum_ind A B (fun x : sum A B => C x (sum_ind A B P IHinl IHinr x))
(fun (x : A) => equation sum_ind_inl in
(f (inl A B x) (IHinl x) :: C (inl A B x) (sum_ind A B P IHinl IHinr (inl A B x))))
(fun (x : B) => equation sum_ind_inr in
(f (inr A B x) (IHinr x) :: C (inr A B x) (sum_ind A B P IHinl IHinr (inr A B x))))
x
== f x (sum_ind A B P IHinl IHinr x).
Definition sum_half_eta :=
fun (A B : Type) (x : sum A B) =>
sum_match_commutes A B (fun (x : sum A B) => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) (fun (x : sum A B) (_ : sum A B) => sum A B) (fun (x : sum A B) (_ : sum A B) => x) x
:: sum_ind A B (fun _ : sum A B => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) x == x.
Rewrite sum_half_eta.
(*********)$ time ./brazil.byte examples/sum.br
...
real 0m1.560s
user 0m1.531s
sys 0m0.031s
$ time ./brazil.byte examples/sum.br
...
real 0m0.333s
user 0m0.311s
sys 0m0.000sBy contrast, timing the smoketest (only the typechecking, not compiling brazil and tt themselves) gives
real 0m0.152s
user 0m0.030s
sys 0m0.091s
on my machine.
It's possible to report either an Error.runtime or an Error.typing error, but there's probably no difference between these two, is there?
An empty input line should not be a syntax error.
Chris asked what sort of equality rules should hold for names (elements of universes). I'd say the following:
U i to U j to U k is the same as coercing from U i to U k, and coercing from U i to U i does nothing.I don't think we want anything else, do we?
Definition bar := { 1 = Universe f0 }.
Definition baz := { fst = Universe f0 }.fst.both work fine but
Definition foo := { 1 = Universe f0 }.1.doesn't.
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 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.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
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.