Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Jul 13 2021 11:54

    dependabot[bot] on bundler

    (compare)

  • Jul 13 2021 11:53

    siddhartha-gadgil on master

    Bump addressable from 2.5.2 to … Merge pull request #285 from si… (compare)

  • Jul 13 2021 11:53
    siddhartha-gadgil closed #285
  • Jul 13 2021 01:13
    dependabot[bot] labeled #285
  • Jul 13 2021 01:13
    dependabot[bot] opened #285
  • Jul 13 2021 01:13

    dependabot[bot] on bundler

    Bump addressable from 2.5.2 to … (compare)

  • Jul 13 2021 01:12

    dependabot[bot] on bundler

    (compare)

  • Jul 13 2021 01:12

    siddhartha-gadgil on master

    Bump addressable from 2.5.2 to … Merge pull request #284 from si… (compare)

  • Jul 13 2021 01:12
    siddhartha-gadgil closed #284
  • Jul 13 2021 01:03
    dependabot[bot] labeled #284
  • Jul 13 2021 01:03
    dependabot[bot] opened #284
  • Jul 13 2021 01:03

    dependabot[bot] on bundler

    Bump addressable from 2.5.2 to … (compare)

  • Mar 01 2020 03:32

    dependabot[bot] on bundler

    (compare)

  • Mar 01 2020 03:32

    siddhartha-gadgil on master

    Bump rake from 12.0.0 to 12.3.3… Merge pull request #283 from si… (compare)

  • Mar 01 2020 03:32
    siddhartha-gadgil closed #283
  • Mar 01 2020 01:50
    dependabot[bot] labeled #283
  • Mar 01 2020 01:50
    dependabot[bot] opened #283
  • Mar 01 2020 01:50

    dependabot[bot] on bundler

    Bump rake from 12.0.0 to 12.3.3… (compare)

  • Mar 01 2020 01:50

    dependabot[bot] on bundler

    (compare)

  • Mar 01 2020 01:50

    siddhartha-gadgil on master

    Bump rake from 12.0.0 to 12.3.3… Merge pull request #282 from si… (compare)

Siddhartha Gadgil
@siddhartha-gadgil
Questions about LTS2019 welome.
Adithya Upadhya
@adithyaupadhya
How do you write a type that shows that an implication implies its contrapositive? The type of such a thing looks like this, I suppose : impliesContrapositive : (A : Type) -> (B : Type) -> (A -> B) -> ((B -> Void) -> (A -> Void))
Is such a thing possible to write, or is it preferable to do a different thing to achieve the same result?
Siddhartha Gadgil
@siddhartha-gadgil
The law of excluded middle is not normally part of the foundations, and is needed for contrapositive being equivalent to the statement. The reason we don't have it is that it does not give a concrete value, and we want concrete values.
By the law of excluded middle for the type $A$ is $A \oplus (A \to Void)$
A(A0)A \oplus (A \to 0)
Here, I meant the 0 type , so should have said
lem(A)=A(A0lem(A) = A \oplus (A \to \mathbb{0}
Sorry,
$$lem(A)= A \oplus (A \to \mathbb{0})
lem(A)=A(A0)lem(A)= A \oplus (A \to \mathbb{0})
Siddhartha Gadgil
@siddhartha-gadgil
The contrapositive in the form you said it is true though,
(AB)(B0)(A0)(A \to B) \to (B \to 0) \to (A \to 0)
This can be proved, i.e., we get a term
(f:AB)(c:B0)a:Ac(f(a)) (f : A \to B) \mapsto (c : B \to \mathbb{0}) \mapsto a : A \mapsto c(f(a))
bnag098
@bnag098

I am having some trouble in using the replace function.
I was trying to substitute $ 0 $ using the equality 0=b0 0 = b \cdot 0 in c=0+c c = 0 + c to hopefully get c=b0+c c = b \cdot 0 + c .
But in the function call below:

replace (sym (multZeroRightZero b)) (sym (plusZeroLeftNeutral c))

I am getting an error claiming that in the second variable of replace, idris expects a value of the type P 0. The documentation on this P function couldn't explain much. Any help here would be appreciated.

SS-C4
@SS-C4
Is it possible to case split on a dependent pair?
For example, if I want to use the pair (x **pf) in a function, where I want to case split on x being Z or (S k), and I need the proof when this happens.
case (fst (x**pf)) of typechecks, but the proof type does not change, and stays the same as the original.
SS-C4
@SS-C4
Oh, I found it. with helps here.
Adithya Upadhya
@adithyaupadhya
To capture the notion of a total order, in which exactly one of three things can occur, a<=b and !(a>=b), !(a<=b) and (a>=b) or (a<=b) and (a>=b), would the best thing to do be to define a new type along the lines of Either, or would it be better to try to work with existing types to get something with the same behaviour?
Siddhartha Gadgil
@siddhartha-gadgil
Generally best to define a new type, though this one may be in the standard library or contrib (look for trichotomy).
Using combinations of pairs, dependent pairs and coproducts (Either) makes stuff hard to understand, parse by idris and also more error-prone (a wrong type may be accepted because of the same structure).
Adithya Upadhya
@adithyaupadhya
Would it be preferable to define the order on the naturals as arising from addition rather than the inductive one defined in the standard library?
Siddhartha Gadgil
@siddhartha-gadgil
Yes, it may work better. In any case if you prove the two are equivalent,
you can use both definitions
shafilmaheenn
@shafilmaheenn
Is there a way to check whether 2 functions have the same name in the entire code folder?
Siddhartha Gadgil
@siddhartha-gadgil
Atom has a search in folder, ctrl-shift-f, which can also be filtered, here using *.idr for filename
shafilmaheenn
@shafilmaheenn
As a lot of theorems about gcd need the bezout's lemma, may I use assert_total in the bez and GCDCalc function which essentially follow Euclid's algorithm?. I have no clue on how to convince idris that Euclid's algorithm is total without that.
Siddhartha Gadgil
@siddhartha-gadgil
Sure. But eventually we will fix this.
Siddhartha Gadgil
@siddhartha-gadgil
I have written and posted a total gcd calculator as BoundedGCD.idr.
Adithya Upadhya
@adithyaupadhya
Could we possibly get a summary of what has been completed so far and what remains to be done? I don't know where to pick up from and the amount of code that is up makes it hard to tell.
shafilmaheenn
@shafilmaheenn
you can read our reports to get a rough idea.
fundamental theorem of arithmetic remains to be done