agda/examples/outdated-and-incorrect/ProofRep.agda

module ProofRep where

import Prelude
import Logic.Relations
import Logic.Identity
import Data.Nat
import Data.Nat.Properties

open Prelude
open Data.Nat hiding (_==_; _≡_)
open Data.Nat.Properties
open Logic.Relations

module Foo (Var : Set) where

  data _==_ : (x y : Var) -> Set where
    cRefl  : {x : Var} -> x == x
    cSym   : {x y : Var} -> y == x -> x == y
    cTrans : {x y z : Var} -> x == z -> z == y -> x == y
    cAxiom : {x y : Var} -> x == y

  data Axioms {A : Set}(_≈_ : Rel A)([_] : Var -> A) : Set where
    noAxioms   : Axioms _≈_ [_]
    anAxiom    : (x y : Var) -> [ x ] ≈ [ y ] -> Axioms _≈_ [_]
    manyAxioms : Axioms _≈_ [_] -> Axioms _≈_ [_] -> Axioms _≈_ [_]

  refl : {x : Var} -> x == x
  refl = cRefl

  sym : {x y : Var} -> x == y -> y == x
  sym (cRefl xy)     = cRefl (Var.sym xy)
  sym  cAxiom        = cSym cAxiom
  sym (cSym p)       = p
  sym (cTrans z p q) = cTrans z (sym q) (sym p)

  trans : {x y z : Var} -> x == y -> y == z -> x == z
  trans {x}{y}{z} (cRefl xy) q     = Var.subst (\w -> w == z) (Var.sym xy) q
  trans {x}{y}{z} p (cRefl yz)     = Var.subst (\w -> x == w) yz p
  trans {x}{y}{z} (cTrans w p q) r = cTrans w p (trans q r)
  trans           p q              = cTrans _ p q