search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
222 stars 18 forks source link

Proofs of symmetry and transitivity for equality in stdlib are broken #72

Closed wilbowma closed 7 years ago

wilbowma commented 7 years ago

Fix for #71 exposed a bug in equality. The test for equality is failing, but the failure seems to indicate that the proof was incorrect previously, but type checked due to #71. Here's the equivalent proof in Coq, which doesn't type check:

Inductive Eq (A : Set) : A -> A -> Set :=
  refl : forall a, Eq A a a.

Definition sym A x y (e : (Eq A x y)) : (Eq A y x) :=
  Eq_rec A
         (fun a => fun b => fun e => (Eq A y x))
         (fun c => (refl A y))
         x
         y
         e.

Definition trans A x y z (e1 : (Eq A x y)) (e2 : (Eq A y z)) : (Eq A x z) :=
  Eq_rec A
         (fun a => fun b => fun e => (Eq A b z))
         (fun c =>
            (Eq_rec A
                    (fun a => fun b => fun e => (Eq A b z))
                    (fun c =>
                       (refl A z))
                    e2))
         e1.