inversion.rkt

#lang cur
(require cur/stdlib/equality
         cur/stdlib/sugar
         cur/stdlib/nat
         cur/stdlib/prop
         cur/ntac/base
         cur/ntac/standard
         cur/ntac/rewrite
         rackunit/turnstile+
         "rackunit-ntac.rkt")

;; tests for inversion tactic

;; successors-equal-implies-equal ----------

(define-theorem successors-equal-implies-equal
 (Π [n : Nat] [m : Nat]
    (-> (== Nat (s n) (s m))
        (== Nat n m)))
 (by-intros n m H)
 (by-inversion H #:as H0)
 (by-rewrite H0)
 reflexivity)

(check-type successors-equal-implies-equal
            :  (Π [n : Nat] [m : Nat]
                  (-> (== Nat (s n) (s m)) (== Nat n m))))

;; successors-equal-implies-equal, raw term
;; not suitable for tactic because it does not include intermediate equalities
;; computed by inversion, eg (== n m)
(check-type
 (λ [n : Nat] [m : Nat]
    (λ [H : (== Nat (s n) (s m))]
      (f-equal
       Nat Nat
       (λ [n : Nat]
         (new-elim
          n
          (λ n Nat)
          n
          (λ n-1 IH n-1)))
       (s n) (s m)
       H)))
 : (Π [n : Nat] [m : Nat]
      (-> (== Nat (s n) (s m)) (== Nat n m))))


;; successors-equal-implies-equal, raw term, produced by coq
(check-type
 (λ [n : Nat] [m : Nat]
    [H : (== Nat (s n) (s m))]
    ((λ [H0 : (-> (== Nat (s m) (s m))
                  (== Nat n m))]
       (H0 (refl Nat (s m))))
     (new-elim
      H
      (λ y h
         (-> (== Nat y (s m))
             (== Nat n m)))
      (λ [H0 : (== Nat (s n) (s m))]
        ((λ [H1 : (== Nat (s n) (s m))]
           ((λ [H2 : (== Nat n m)]
              ((λ [H3 : (== Nat n m)]
                 (new-elim
                  (sym Nat n m H3)
                  (λ n0 h (== Nat n0 m))
                  (refl Nat m)))
               H2))
            (f-equal
             Nat Nat
             (λ [e : Nat]
               (new-elim
                e
                (λ x Nat)
                n
                (λ n-1 ih n-1)))
             (s n) (s m)
             H1))
           )
         H0)))))
 : (Π [n : Nat] [m : Nat]
      (-> (== Nat (s n) (s m))
          (== Nat n m))))

;; successors-equal-implies-equal, raw term, produced by coq, simplified1
(check-type
 (λ [n : Nat] [m : Nat]
    [H : (== Nat (s n) (s m))]
    ((λ [H3 : (== Nat n m)]
       (new-elim
        (sym Nat n m H3)
        (λ n0 h (== Nat n0 m))
        (refl Nat m)))
     (f-equal
      Nat Nat
      (λ [e : Nat]
        (new-elim
         e
         (λ x Nat)
         n
         (λ n-1 ih n-1)))
      (s n) (s m)
      H)))
 : (Π [n : Nat] [m : Nat]
      (-> (== Nat (s n) (s m))
          (== Nat n m))))

;; one-neq-zero ----------

(define-theorem one-neq-zero
  (-> (== Nat (s 0) 0) False)
  (by-intro H)
  (by-inversion H))

(check-type one-neq-zero : (-> (== Nat (s 0) 0) False))

;; one-neq-zero raw term, insufficient for tactic
(check-type
 (λ [H : (== Nat (s 0) 0)]
   (new-elim
    H
    (λ [n : Nat]
      (λ h3
        (new-elim n (λ n Type) False (λ x y True))))
    I))
 : (-> (== Nat (s 0) 0) False))


;; 0 \beq 1 raw term, generated by coq
(check-type
 (λ [H : (== Nat 0 1)]
   ((λ [H0 : (-> (== Nat 1 1) False)] (H0 (refl Nat 1)))
    (new-elim
     H
     (λ y h (-> (== Nat y 1) False))
     (λ [H0 : (== Nat 0 1)]
       ((λ [H1 : (== Nat 0 1)]
          ((λ [H2 : False] ((λ [H3 : False] (new-elim H3 (λ x False))) H2))
           (new-elim
            H1
            (λ x h
               (new-elim x (λ x Type) True (λ x y False)))
            I)))
        H0)))))
 : (-> (== Nat 0 1) False))

;; 0 \beq 1 raw term, generated by coq, simplified1
(check-type
 (λ [H : (== Nat 0 1)]
   ((λ [H0 : (-> (== Nat 1 1) False)] (H0 (refl Nat 1)))
    (new-elim
     H
     (λ y h (-> (== Nat y 1) False))
     (λ [H0 : (== Nat 0 1)]
       ((λ [H1 : (== Nat 0 1)]
          ((λ [H2 : False] (new-elim H2 (λ x False))) ; elim-False should produce this
           (new-elim
            H1
            (λ x h
               (new-elim x (λ x Type) True (λ x y False)))
            I)))
        H0)))))
 : (-> (== Nat 0 1) False))

;; 0 \beq 1 raw term, generated by coq, simplified2
(check-type
 (λ [H : (== Nat 0 1)]
   ((λ [H2 : False] (new-elim H2 (λ x False))) ; elim-False should produce this
    (new-elim
     H
     (λ x h
        (new-elim x (λ x Type) True (λ x y False)))
     I)))
 : (-> (== Nat 0 1) False))

;; 0 beq q raw term, generated by ntac
(check-type
 (λ (H : (== Nat (s z) z))
   ((λ (H54 : False) H54)
    (new-elim H (λ x h (new-elim x (λ x Type) False (λ x y True))) I)))
 : (-> (== Nat (s z) z) False))

;; variations of one-neq-zero: ----------
;; - testing ntac generation of False term

(define-theorem zero-neq-one
  (-> (== Nat 0 (s 0)) False)
  (by-intro H)
  (by-inversion H))

(check-type zero-neq-one : (-> (== Nat 0 (s 0)) False))

(define-theorem zero-neq-two
  (-> (== Nat 0 2) False)
  (by-intro H)
  (by-inversion H))

(check-type zero-neq-two : (-> (== Nat 0 2) False))

;; tests elim-False
(define-theorem two-neq-three
 (-> (== Nat (s 0) 0)
     (== Nat (s (s 0)) (s (s (s 0)))))
 (by-intro H)
 elim-False
 (by-inversion H))

(check-type two-neq-three
 : (-> (== Nat (s 0) 0)
     (== Nat (s (s 0)) (s (s (s 0))))))

;; new: eliminates cases, even if goal isn't False
(define-theorem two-neq-four
 (-> (== Nat (s 0) 0)
     (== Nat (s (s 0)) (s (s (s 0)))))
  (by-intro H)
  (by-inversion H))

(check-type two-neq-four
 : (-> (== Nat (s 0) 0)
     (== Nat (s (s 0)) (s (s (s 0))))))