Trouble proving that 2 does not divide 1

[scott....@gmail.com]

Hi Idris folks,

I wrote a data type Divides:

data Divides : (m : Nat) -> Nat -> Type where
  Zero : Divides m Z
  Next : {p : Nat} -> Divides m p -> Divides m (m + p)

I can prove that any number divides zero, that one divides any
number, that 2 divides 4, and that 3 divides 15.  So far, so
good.

I am trying to prove that 2 does not divide 1.

twoNotDivideOne : Divides 2 1 -> Void
twoNotDivideOne x = ?twoNotDivideOne_rhs

By case-splitting on the x, Idris fills in that both cases are
impossible.  I could believe this.

twoNotDivideOne : Divides 2 1 -> Void
twoNotDivideOne Zero impossible
twoNotDivideOne (Next _) impossible

But when I go to load the code, I get this error:

- + Errors (1)
 `-- DividesSmall.idr line 7 col 25:
     twoNotDivideOne (Next _) is a valid case

So I try to write a proof for the second case.

twoNotDivideOne : Divides 2 1 -> Void
twoNotDivideOne Zero impossible
twoNotDivideOne (Next prf) = ?a

When I load the code to see the type wanted for the hole, I get
this error:

- + Errors (1)
 `-- DividesSmall.idr line 7 col 0:
     When checking left hand side of twoNotDivideOne:
     When checking an application of Main.twoNotDivideOne:
             Type mismatch between
                     Divides m (m + p) (Type of Next _)
             and
                     Divides 2 1 (Expected type)
             
             Specifically:
                     Type mismatch between
                             S p
                     and
                             0

I'm sure this is the kind of thing that seasoned Idrisers run
into all the time.  Could someone give me a hint?

I'm using Idris 1.3.3.

Thanks,

Scott

[Denis Buzdalov]

Hi Scott,

I'm sure this is the kind of thing that seasoned Idrisers run
into all the time.  Could someone give me a hint?

I'm using Idris 1.3.3.

I'm sorry for not answering your question directly, but I can say that the modern Idris 2 typecheks

twoNotDivideOne : Divides 2 1 -> Void                      

twoNotDivideOne Zero impossible                            
twoNotDivideOne (Next _) impossible

without any problem. Possibly, it is a bug in Idris 1 and since the old version is not supported, it's unlikely to be fixed.

Denis

[Robert Watson]

As a fairly new user I find it fascinating that Idris2 will work with just this:

twoNotDivideOne : Divides 2 1 -> Void                      

twoNotDivideOne Zero impossible 

But that if, Scott, you had defined Next as:

Next : {p : Nat} -> Divides m p -> Divides m (p + m)

you'd have counter-intuitively (to me at least) more work proving it, and it feels like you are blocked by some arbitrary constraint, just as when you get it the right way round it seems magical in its automaticity. Proof complexity is very dependent on the initial definitions, on the implementations, in this case the asymmetry in the definition of 'plus'.  This can be very frustrating if you want something more like the abstractions of regular mathematics (or like me want to do computer algebra with Idris2) where the above two definitions should be the same. But I actually think this is a fundamental issue we have to really explore (intrinsic versus extrinsic?). I'm using interfaces for that level of abstraction. I think it would be a mistake to somehow make things more extrinsic (?) too early.

I'd be very interested if folks have insight into this.

Rob

[Robert Watson]

I think the terminology is intensional versus extensional...sorry.

R

[Jacob Thomas Errington]

I've always heard of intensional vs extensional as (roughly speaking) "identical" vs "behaviourally indistinguishable".

On the other hand, "intrinsic" definitions usually carry a property directly within themselves. For example, an intrinsicially-typed formulation of STLC means that the definition of the syntax of terms carries the types of the terms directly within it. This is as opposed to an extrinsically-typed setup in which there are raw terms separate from typing derivations relating terms to types.

I'll write my example in Beluga since I don't need to mess with contexts that way.

LF tp : type =
  | base : tp
  | arr : tp -> tp -> tp;

LF tm : tp -> type =
  | c : tm base
  | lam : (tm A -> tm B) -> tm (arr A B)
  | app : tm (arr A B) -> tm A -> tm B;

Above, terms are essentially identified with typing derivations.

LF tm' : type =
  | c : tm'
  | lam : (tm' -> tm') -> tm'
  | app : tm' -> tm' -> tm';

LF of_type : tm -> tp -> type =
  | t_c : of_type c base
  | t_lam : ({x : tm'} of_type x A -> of_type (M x) B) -> of_type M (arr A B)
  | t_app : of_type M (arr A B) -> of_type N A -> of_type (app M N) B;

Extrinsic definitions have a certain modularity advantage that intrinsic definitions don't, although they are more annoying / repetitive to create.

Jake

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/0ac0f453-358d-4910-a261-cbb08766834bn%40googlegroups.com.

[David Thrane Christiansen]

tir. 1. jun. 2021 18.33 skrev Jacob Thomas Errington <ja...@mail.jerrington.me>:

I've always heard of intensional vs extensional as (roughly speaking) "identical" vs "behaviourally indistinguishable".

While this basically works from the perspective of functions, I think there's a more fundamental concept at play.

The way I'd describe these concepts is rather as what Frege calls "Sinn" and "Bedeutung" (variously translated as "sense and reference" or "sense and nominatum" ...). The idea is that intensional equality is a sameness of a way of describing a thing, while extensional equality is sameness of the thing itself. Frege's example is that the sentence "the morning star is the evening star" is not a tautology, even though both the morning star and the evening star are ways of referring to Venus.

With respect to functions, we normally consider functions to be sets of tuples. Two lambda expressions that denote the same sets of tuples may be quite different syntactically. Thus, we can have two ways of taking about the same function, or two senses for the same reference, or two intensions for the same extension.

This analysis allows us to talk about what extensional equality would mean for things other than functions. For instance, propositional extensionality equates all proofs of the same proposition. 

Being picky about this kind of thing can help with understanding - or at least it did for me! Hope this is useful rather than annoying.

David

[Robert Watson]

My original terminology was wrong. Jake's clarification is clear. The fundamental concept of Frege is the key idea here. Very cool. But Frege didn't have a 21st century computing device to fiddle with. Why not think about it as the difference between implementations? Something that is implementation specific and structural (closer to CS) being more 'intensional' (so machine code would then be intensional). Something that is abstracted  (closer to the maths understanding or category theory or the application level or a high-level language or whatever) is then more 'extensional'. The sameness of the way of describing a thing is an implementation! In practical terms we want to use more intensional structures when implementing more extensional abstractions (the real thing itself being, say, a game of Pacman, not the details of the emulator). Let me bring this back to Idris and make it real for the more intensionally minded: 

lteMult_lem : LTE 1 q -> mult p b = q -> LTE 1 b

This type definition is mathematically intuitively easy in some sense. From an extensional point of view it's 'obvious'. But 'intensionally' this type definition confounds. Try to have a conversation with Idris2 to complete it! You will have to make very good decisions to avoid a tiff rather than a conversation (it can be done in only two lines though!) The implementation specifics of Idris get in the way at almost every turn I'd say. Any small diversion from the optimum and you are in the weeds, or at least I was. It's very 'dense' in the mismatch between intensional and extensional, in dead-end roads and such like. And the practical implication is that it makes programming harder when we should be trying to make programming easier. That couldn't be more practical and relevant to Idris development.

Rob