4 ms·

One way is to use Functional Extensionality, which is to say that two functions are equal if for all possible inputs they return the same value. In Coq for ins

One way is to use Functional Extensionality, which is to say that two functions are equal if for all possible inputs they return the same value. In Coq for instance. Axiom functional_extensionality: forall {X Y: Type} {f g : X -> Y}, (forall (x: X), f x = g x) -> f = g. Theorem x2_eq_xplus: (fun x => 2 * x) = (fun x => x + x). Proof. apply functional_extensionality. intros. destruct x. - reflexivity. - simpl. rewrite <- plus_n_O. reflexivity. Qed.

theoh 9y ago
Does that work for X being the real numbers?
- BreakfastB0b 9y ago
  I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not. But Haskell's quickCheck doesn't seem to find a problem. λ quickCheck @(Float -> Bool) $ \x -> 2 * x == x + x +++ OK, passed 100 tests. λ quickCheck @(Double -> Bool) $ \x -> 2 * x == x + x +++ OK, passed 100 tests. It doesn't like associativity though. λ quickCheck @(Double -> _) $ \a b c -> (a + b) + c == a + (b + c) *** Failed! Falsifiable (after 6 tests and 4 shrinks): 20.0 3.5741489348898856 2.894651135185324
  - theoh 9y ago
    OK, so those techniques would work equally well on arbitrarily complicated and intractable code examples -- which is useful in practice but not in the spirit of a formal determination of equality. From the perspective of an Agda-phobe: The "2*x vs x+x" example could be a case of a general question about arithmetic expressions, or it could even just be about multiplication and addition. Since multiplication of integers can be defined as repeated addition, proving equality in that particular case for any numeric type just takes a rewrite of both sides in terms of addition only. If the coefficient ("2") was not a natural number, things would be a little more complicated (as other comments mention, you'd have to introduce some way of getting things into a canonical form). I guess that would be an "intensional" approach. The best story I have about extensional definitions is a true one. At a class on bike repair, somebody asked what a fixed-wheel bike was. The instructor started to give an extensional definition: "It's like... a unicycle." Presumably he could have followed this with other examples such as a Penny Farthing -- but the audience seemed satisfied. It would obviously have been more helpful to give an intensional definition ("no gears".)
  - seanwilson 9y ago
    > I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not. It would work with Coq's real number type but as the same properties wouldn't always hold with hardware float types, you may have trouble running the program if you extracted it to e.g. Haskell (as your example shows)? The QuickCheck tests would pass if you allowed a small difference between them to account for floating point inaccuracies I imagine.
  - Veedrac 9y ago
    In IEEE 2 * x == x + x, which follows from the basic premise that these operations are correct to the nearest float.
- LolWolf 9y ago
  It works in the sense that there are finite number of them on a finite-size machine, but exhaustion would be infeasible in almost all possible cases.
- chriswarbo 9y ago
  Yes. When we see a universal quantifier (e.g. 'forall (x : X)...') it's tempting to think that we're talking about the thing being quantified over (i.e. 'X'), but in fact what we're saying is that the quantified thing is irrelevant. In the case of something like `\x. 2 * x` and `\x. x + x`, we're saying "forget about what 'x' might be, because it's irrelevant; look, I'll show you that we can use semantics-preserving rewrite rules to turn one of these syntax trees into the other". The resulting theorems work for all 'x' precisely because the proof doesn't need to know or care what the value of 'x' is, since it's just shuffled around as a symbol (part of the syntax tree).

theoh 9y ago

Does that work for X being the real numbers?

BreakfastB0b 9y ago
I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not. But Haskell's quickCheck doesn't seem to find a problem. λ quickCheck @(Float -> Bool) $ \x -> 2 * x == x + x +++ OK, passed 100 tests. λ quickCheck @(Double -> Bool) $ \x -> 2 * x == x + x +++ OK, passed 100 tests. It doesn't like associativity though. λ quickCheck @(Double -> _) $ \a b c -> (a + b) + c == a + (b + c) *** Failed! Falsifiable (after 6 tests and 4 shrinks): 20.0 3.5741489348898856 2.894651135185324
- theoh 9y ago
  OK, so those techniques would work equally well on arbitrarily complicated and intractable code examples -- which is useful in practice but not in the spirit of a formal determination of equality. From the perspective of an Agda-phobe: The "2*x vs x+x" example could be a case of a general question about arithmetic expressions, or it could even just be about multiplication and addition. Since multiplication of integers can be defined as repeated addition, proving equality in that particular case for any numeric type just takes a rewrite of both sides in terms of addition only. If the coefficient ("2") was not a natural number, things would be a little more complicated (as other comments mention, you'd have to introduce some way of getting things into a canonical form). I guess that would be an "intensional" approach. The best story I have about extensional definitions is a true one. At a class on bike repair, somebody asked what a fixed-wheel bike was. The instructor started to give an extensional definition: "It's like... a unicycle." Presumably he could have followed this with other examples such as a Penny Farthing -- but the audience seemed satisfied. It would obviously have been more helpful to give an intensional definition ("no gears".)
- seanwilson 9y ago
  > I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not. It would work with Coq's real number type but as the same properties wouldn't always hold with hardware float types, you may have trouble running the program if you extracted it to e.g. Haskell (as your example shows)? The QuickCheck tests would pass if you allowed a small difference between them to account for floating point inaccuracies I imagine.
- Veedrac 9y ago
  In IEEE 2 * x == x + x, which follows from the basic premise that these operations are correct to the nearest float.
LolWolf 9y ago
It works in the sense that there are finite number of them on a finite-size machine, but exhaustion would be infeasible in almost all possible cases.
chriswarbo 9y ago
Yes. When we see a universal quantifier (e.g. 'forall (x : X)...') it's tempting to think that we're talking about the thing being quantified over (i.e. 'X'), but in fact what we're saying is that the quantified thing is irrelevant. In the case of something like `\x. 2 * x` and `\x. x + x`, we're saying "forget about what 'x' might be, because it's irrelevant; look, I'll show you that we can use semantics-preserving rewrite rules to turn one of these syntax trees into the other". The resulting theorems work for all 'x' precisely because the proof doesn't need to know or care what the value of 'x' is, since it's just shuffled around as a symbol (part of the syntax tree).