Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 121fe1238c
Fetching contributors…

Octocat-spinner-32-eaf2f5

Cannot retrieve contributors at this time

file 90 lines (86 sloc) 1.993 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
{-# SKIP #-}
module Lem.EqNatTrans where

-- Transitivity of 'eqNat'.
--
-- Not true for non-CF args, e.g.
--
-- S UNR `eqNat` UNR = UNR
--
-- and
--
-- UNR `eqNat` BAD = UNR
--
-- but
--
-- S UNR `eqNat` BAD = BAD.
--
-- It's true for CF args.
--
-- It's interesting to note that we don't seem to be able to talk
-- about contradictions directly. For example, we know that
--
-- x `eqNat` y
--
-- and
--
-- x = S x_
--
-- then
--
-- y = UNR \/ y = S y_,
--
-- and in particular
--
-- y /= Zero.
--
-- But we can't actually state this, and for good reason: we lose
-- probably soundness if we're allowed to talk about negation, because
-- of our "induction up to UNR". E.g.
--
-- f ::: c
-- f ::: ~ c
-- f = f
--
-- would check and then we'd have something like '(f in c) /\ ~ (f in c)'.
--
-- However, we don't need induction to prove
--
-- y /= Zero,
--
-- so the following proof works.
import Lib.Arithmetic ;;

lem_eqNat_trans x y z = case x of {
; Zero -> case y of {
          ; Zero -> case z of {
-- x = z = Zero -> x `eqNat` z = Zero `eqNat` Zero
                    ; Zero -> QED
-- contra: x = Zero,
-- z = Succ z_,
-- and so Zero `eqNat` Succ z_ = False,
-- but we assume x `eqNat` z is not False.
                    ; Succ z_ -> QED -- contra
                    }
          ; Succ y_ -> QED -- contra
          }
; Succ x_ -> case y of {
             ; Zero -> QED -- contra
             ; Succ y_ -> case z of {
                          ; Zero -> QED -- contra
-- For any 'a' and 'b' have
--
-- (1) Succ a `eqNat` Succ b = a `eqNat` b
--
-- and so we can apply IH to 'x_', 'y_', 'z_', giving
--
-- x_ `eqNat` z_,
--
-- but then done, again by (1).
                          ; Succ z_ -> lem_eqNat_trans x_ y_ z_
                          }
             }
};;

{-# CONTRACT
lem_eqNat_trans ::: x:CF -> y:(CF&&{y: x `eqNat` y})
-> z:(CF&&{z: y `eqNat` z})
-> CF&&{qed: x `eqNat` z}
#-};;
Something went wrong with that request. Please try again.