Idris has a way to present equalities like this: addition_unit : (a:Nat) -> (a + 0) = a addition_s : (a,b:Nat) -> (a + S b) = S (a + b) add_commutative : (a,b:Nat) -> (a + b = b + a)
They can be used to prove more things: try_out : (x,y:Nat) -> ((x + 0) + y) = y + x try_out x y = rewrite addition_unit x in add_commutative x y It's rewriting the left expression to right expression, though you can easily flip the direction. For clarity I show these few dissections: try_out x y = ?a1 a1 : plus (plus x 0) y = plus y x try_out x y = rewrite addition_unit x in ?a2 a2 : plus x y = plus y x Idris has this feature called "Elaborator reflection". It allows you to describe automated tactics for writing proofs/programs. The "getGoal" and "getEnv" allow you to examine types in the context: getGoal : Elab (TTName, TT) getEnv : Elab (List (TTName, Binder TT)) The elaborator reflection also allows accessing the term rewriting. I suppose that's all you need in order to write a program that simplifies equations inside the type context? -- Henri Tuhola On Sat, 21 Sep 2019 at 11:50, Martin Baker <ax87...@martinb.com> wrote: > > I'm a fan of both Axiom and Idris. I think my ideal would be Axiom > mathematics build on top of the Idris type system. > > The Axiom type system was incredibly advanced for its time but I suspect > the Idris type system has finally caught up and overtaken it? Correct me > if I'm wrong but I think the Axiom type system does not have the > following capabilities that Idris does: > > * Enforcement of pure functions. > * Ability to flag a function as total as opposed to partial (automatic > in some cases). > * Universes (types of types hierarchy). > > I'm no expert but I would have guessed these things would be almost > indispensable for proving Axiom correct? > > Also Idris makes it far more practical to use these things, I don't > think Axiom can implement category theory constructs like monads. Also, > although both have dependent types, Axiom does not use them for say, > preventing the addition of a 2D vector to a 3D vector. In Idris this is > more likely to be compile time error than a runtime error, I know there > are theoretical limits to this but I think Idris has capabilities to > make this practical in more cases. > > I don't pretend I know how an Idris type system could be used with Axiom > in practice. For instance I think the proofs Henri is talking about are > equalities in the type system (propositions as types). So how would > these equations relate to equations acted on by equation solvers (which > might be an element of some equation type). Could there be some way to > lift equations into the type system and back? > > Sorry if I'm confusing things here but I just have an intuition that > there is something even more powerful here if all this could be put > together. > > Martin > > On 21/09/2019 04:28, Tim Daly wrote: > > Axiom has type information everywhere. It is strongly > > dependently typed. So give a Polynomial type, which > > Axiom has, over a Ring or Field, such as > > Polynomial(Integer) or Polynomial(Fraction(Integer)) > > we can use theorems from the Ring while proving > > properties of Polynomials. > > _______________________________________________ > Axiom-developer mailing list > Axiom-developer@nongnu.org > https://lists.nongnu.org/mailman/listinfo/axiom-developer _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer