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 has a deep type hierarchy, all of which can be inherited by types like Polynomial. The type hierarchy uses Group Theory as its scaffold. I'm "decorating" the inherited type hierarchy with axioms. These will be available by inheritance for Polynomial proofs. Proving GCD in non-negative integers can assume that all of the arguments are non-negative integers (i.e. NATs). There are quite a few GCD algorithms in Axiom. I'm trying to prove the implemented algorithms for GCD correct rather than rewrite them. I've seen a couple of the Idris videos. It looks quite interesting. Given an Idris proof, is there a "verifier" function? Tim On 9/20/19, Henri Tuhola <henri.tuh...@gmail.com> wrote: > I doubt it does cover that. And I think there would be at least two > approaches to implement GCD for polynomials in Idris. > > Obvious approach would be to construct a type that represents > polynomials on some base number and variables. For example, > (Polynomial Nat [X]). You would then prove GCD for this structure. > > Another approach I can think of would exploit the way how > type-propositions themselves can cause computer-algebra-system -like > behavior, reusing variables that the type system is already working > with. You can prove (a = b) -> (b = c) -> (a = c), then compose > equations together with that. Similarly you can rewrite x to y inside > a type if you have (x = y). There's already some support for changing > the behavior of Idris type checker, it could be that some sort of > equation simplifier could be implemented with features that Idris > already has. > > -- Henri Tuhola > _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer