Does the Idris code cover GCD for polynomials?
On 9/20/19, Henri Tuhola <henri.tuh...@gmail.com> wrote: > You can already define and prove gcd in idris/agda/coq. It's not too hard > either. > > This weekend I am trying to prove transitive closure can be computed in > Idris. The way I represent it is that I have f:(a -> a -> Type), this forms > a type that is inhabited when a statement is true. I can wrap this into > another type that represents transitiveness. I can get (Transitive f x), > from which I can make a set: (Set (Transitive f x)). This type describes a > set containing all symbols reachable from 'x', through some way they relate > 'f'. > > Idris has some flaws that annoy when using it. Those issues become clear > when trying to prove injectivity for certain sort or functions that have > multiple variables. Also it's sometimes quite dumb, forgetting how values > computed too early and other times is remembers that quite too well. > > -- Henri Tuhola > > pe 20. syysk. 2019 klo 8.56 Tim Daly <axiom...@gmail.com> kirjoitti: > >> https://www.youtube.com/watch?v=uLCqJLFP7f8 >> >> The above link is about SEL4, the proven kernel. >> They have about 1 million lines of proof. >> >> I've been looking at the issue of "proof down to the metal". >> It seems that SEL4 will run on an ARM processor which >> is the basis for the Raspberry PI. I have a PI and am looking >> to boot SEL4. >> >> There is also the proven lisp stack which I've previously >> mentioned. >> >> It seems that it may be possible (in the next hundred years?) >> to have an Axiom image that proves the GCD algorithms all >> the way to the metal. >> >> The search continues... >> >> Tim >> >> _______________________________________________ >> 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