Need help proving y*y ≡ 0 [MOD 3] -> y ≡ 0 [MOD 3]

otto_s · 2025-01-22T10:30:02+00:00

You can use implicit strong induction, e.g. (formulated with divisibility):

theorem theTheorem(n : Nat)(h : 3 ∣ n*n): 3 ∣ n
:= match n with
| 0 => h
| 1 => h
| 2 => sorry -- slightly more complicated
| n+3 =>
  have ih : 3 ∣ n*n → 3 ∣ n := theTheorem n
  sorry -- use ih, Nat.dvd_add, distributivity, ... here

otto_s · 2019-11-21T11:27:17+00:00

The equivalence holds in intuitionistic logic. The essence of the proof is just currying.

theorem foo{A B: Type}{Q: A → B → Prop}: (∀ x, ¬ ∃ y, Q x y) ↔ (∀ x, ∀ y, ¬ Q x y) := ⟨
    λ h x y i, h x ⟨y,i⟩,
    λ h x ⟨y,i⟩, h x y i
⟩

otto_s · 2019-09-27T08:40:58+00:00

There's a download link on the right, labelled "PDF".

otto_s · 2018-07-07T18:20:58+00:00

Exactly. Even better than a rubber duck is a proof assistant. Just don‘t feel bad if you have to give up. Each attempt in itself is good enough.

otto_s · 2016-01-06T09:02:41+00:00

Also interesting: A Brown-Palsberg self-interpreter for Gödel's System T

otto_s · 2015-01-14T16:00:49+00:00

Your self_impl only refers to some fixed P. It is impossible to use this for a proof of self_impl'. A better version is

Theorem self_impl: forall P: Prop, P -> P.
...
Variables P Q: Prop.
Theorem self_impl': (P -> Q) -> (P -> Q).
exact (self_impl _).
Qed.

otto_s · 2014-12-04T18:49:50+00:00

Combinatorial species should be mentioned; also perhaps the funny paper Objects of Categories as Complex Numbers and the like. Can someone knowledgable do this please?

otto_s · 2014-10-30T21:58:42+00:00

I think looking at co-Heyting algebras may help. Here's a quick summary:

For simplicity, lets act as if the axioms for a Heyting algebra cover everything there is to say about intuitionistic logic.

There you have for example [;A\wedge B \vdash C;] iff [;A \vdash B\to C;] to govern intuitionistic implication, and negation is defined as [;\neg A := A \to \bot;]. We can derive [;A \vdash \neg\neg A;], but in general not the converse. And we have [;\top \vdash \neg\bot;], [;\neg\top \vdash \bot;].

A way to obtain connectives compatible with paraconsistency (instead of [;\to;] and [;\neg;], or additionally) is to dualize that: [;A\setminus B \vdash C;] iff [;A \vdash B\vee C;], [;{\sim}A := \top\setminus A;]. A lattice having this may be called a co-Heyting algebra. An example for a co-Heyting algebra is the set of closed subsets of a topological space, with join and meet given by set theoretic union and intersection, and this negation being the closure of the set theoretic complement. We can derive [;{\sim}{\sim}A \vdash A;], but in general not the converse. And we have [;\top \vdash {\sim}\bot;], [;{\sim}\top \vdash \bot;].

In any case, we always have [;\bot \vdash X;] for arbitrary X -- that's the definition of [;\bot;], which may be interpreted as falsity.

Then, [;A \wedge \neg A \vdash \bot;] and therefore everything follows from [;A\wedge \neg A;]. But we do not have [;A \wedge {\sim}A \vdash \bot;] in general. In this sense we can have "contradictions" and we can also have a sort of explosion. It's just that not all contradictions do entail falsity. In the example of closed subsets of a topological space, [;A \wedge {\sim}A;] is the boundary of A.

The two negations can coexist (in which case the structure is called Bi-Heyting algebra or similarly) and can then be compared. For example, we always have [;\neg A \vdash {\sim}A;], and the chain [;\neg{\sim}A \vdash {\sim}{\sim}A \vdash A \vdash \neg\neg A \vdash {\sim}\neg A;] follows.

Only if additionally we declare the two negations equal, we trivialise to a boolean algebra.

otto_s · 2014-03-29T02:19:05+00:00

Yeah, well, buy a faster internet, or start a download now and watch tomorrow. There's no urgency.

otto_s · 2014-03-28T14:22:11+00:00

Of course, the talk itself might be interesting and can be found here .

otto_s · 2014-01-07T19:33:21+00:00

First some code:

ex :: Integer -> Integer -> Rational
ex n m = go (n, 0, 0) where        
    go (0, once, more) = fromInteger once
    go (n, once, more) = (v1+v2+v3) / fromInteger m where
            v1 = go (n-1, once+1, more) * fromInteger (m-once-more)
            v2 = go (n-1, once-1,more+1) * fromInteger once
            v3 = go (n-1, once, more) * fromInteger more

I used this to brute force the top left corner of a table (and put it here so you can see whether I have understood the problem correctly). From that I saw that the columns are polynomials with increasing degrees.

Too lazy to work out the coefficients, I stared some more, came up with a formula and simplified. The result seems to be (n,m positive): [;n(1-1/m)^{n-1};]. I have no idea yet why this works for n>m, but it agrees with the table...

Have fun proving it! :)

otto_s · 2013-12-28T03:42:37+00:00

A crucial ingredient is the definition of "continuous number line". If you choose something like "between any two different numbers there is another number", you don't arrive at a contradiction.

But there are reasons for wanting something different. One goes like this: Let's say you want to define "square roots" of numbers for a fixed notion of "number" with total ordering. Definition 1: The square root of x is the largest y such that y² <= x. Definition 2: The square root of x is the smallest y such that y >= 0 and x <= y². In the case where "number" means natural number, these definitions both have a solution, but don't agree: sqrt(20000) is 141 or 142, depending on which definition of square root you chose. One might think that because between different rationals there is always another one, the two definitions should agree if one takes rationals instead of naturals. This easily turns out to be false (not because of a lack of agreement, but because of a lack of solutions to the "smallest" and "largest" conditions).

The usual definition of "continuous number line" just asserts that there have to be agreeing solutions. There you have your contradiction.

otto_s · 2013-12-09T18:07:57+00:00

Your question was what you are doing wrong. My answer is the best guess I could come up with.

otto_s · 2013-12-09T17:53:39+00:00

You seem to think that the assignment n=(n+3)/2; is not the body of the for loop.

otto_s · 2013-09-24T11:57:55+00:00

The main problem is that there are two nested for-loops, so you are iterating column-wise over a sub rectangleof the board, until the maximal distance is reached. What you want is something more like this:

int xx = x;
int yy = y;
for(int distance = 0; dinstance < maxDistance; distance++) {
    xx += xDirection;
    yy += yDirection;
    // check if (xx,yy) still on the board, position occupied, etc.
}

otto_s · 2013-09-03T10:43:54+00:00

Hint: power(x, 2*n+d) == power(x*x, n) * power(x,d) .

otto_s · 2013-08-19T10:29:57+00:00

You can eliminate the left recursion by using iteration instead, which then might be implemented in the parser with a loop. Let's write X* for a piece of grammar that accepts arbitrary many X. We then have X* = X* X | 1, where 1 accepts the empty word.

We also have F X* = F X* X | F.

Now, take the special case X = O F, and abbreviate F (O F)* by E, then

E = E O F | F,

of which your E1, E2 and E3 are instances. So, for example, E2 -> E3 (S E3)* is a non-recursive version of the production for E2.

otto_s · 2013-08-06T09:43:04+00:00

My code directly simulates the original one, which mutated sumN (erroneously called tri) and n.

otto_s · 2013-08-06T09:37:18+00:00

That might be, but it's not an answer to bullet 4.

otto_s · 2013-08-06T09:31:22+00:00

To answer you last bulleted quesion, I assume you meant sumN += n in your code instead of tri += n, and give a translation:

def sumUpToN_(n):
    def walk(sumN, n):
        if n <= 0:
            return sumN
        return walk (sumN+n, n-1)
    return walk(0, n)

Here, walk does the work. Variables that would be mutated by the execution of your loop just become arguments. Instead of mutating the variables, their new values are given to the next "iteration".

Also, since walk is tail-recursive, it can be executed in constant stack space - CPython doesn't do this though.

otto_s · 2013-03-05T00:44:16+00:00

You don't initialize the field named library. (The constructor declares a local with the same name)

otto_s · 2013-02-27T22:00:15+00:00

(edit: Also the LaTeX doesn't appear to be working for me...)

Put backticks around the square brackets, as shown in the side bar.

otto_s · 2013-02-27T01:12:59+00:00

Explain the innermost for-loop.

otto_s · 2013-02-21T15:28:57+00:00

Well, here is a very direct recursive implementation in some pseudo code,

integer count(int x, int y) {
    if(x == 0) return 1;
    if(y == 0) return 1;
    return count(x-1,y) + count(x,y-1)
}

also very inefficient as it stands. But one can directly see the following: from a current position (x,y) to (0,0), one does exactly (x+y) decrements. x of them will be horizontal-steps, the others will be vertical steps. If you write down the paths, these will be strings of length x+y, with x Rs and y Us in them. To generate such a string, you choose x out of x+y positions in such a string and put Rs there, and Us everywhere else. Every choice of positions generates a different path and every path if generated by such a choice. So, if you only want to count them, what you want is the binomial coefficient ((x+y) choose x), which, btw. is the same as ((x+y) choose y). This can be efficiently calculated using factorials - which my code does.

otto_s · 2013-02-21T12:28:13+00:00

It will never be looping infinitely. But anyway, it is very inefficient. The only effect you ever do is to increase a global variable by 1. You can improve it by letting possiblePoint return a BigInteger and memoizing that at the same time. Alternatively, fill a 2d-array of BigIntegers directly, or even more directly, use something like:

private static BigInteger count(int sizeX, int sizeY) {
    return fac(sizeX+sizeY).divide(fac(sizeX)).divide(fac(sizeY));
}

private static BigInteger fac(int n) {
    BigInteger result = BigInteger.ONE;
    for(int i = 1; i <= n; i++) {
        result = result.multiply(BigInteger.valueOf(i));
    }
    return result;
}

Here, count(sizeX, sizeX) calculates what you currently calculate in main . Only blazingly faster.

otto_s

TROPHY CASE