formality-proofs-example.fm

import Base@0

// Etapa 1: vê o tipo do "e" (no caso, `0 == 1`)
// Etapa 2: troca "x" no template pela esquerda do "e" (no caso, fica "P(0)")
// Etapa 3: verifica se o "p" tem o tipo "P(0)"
// Etapa 4: se sim, ele troca "x" no template pela direita do "e" (no caso, fica "P(1)")
// Etapa 5: muda o tipo do "p" pra "P(1)"
exemplo : {e : 0 == 1, p : P(0)} -> P(1)
  p :: rewrite x in P(x) with e

P : {x : Word} -> Type
  Word

p0 : {a : Word, b : Word, e : a == b, p : P(a)} -> P(b)
  p :: rewrite x in P(x) with e

p1 : {a : Word, b : Word, e : a == b} -> b == a
  refl(~a) :: rewrite x in x == a with e

p2 : {e : 0 == 1, p : P(0)} -> P(2)
  p :: rewrite x in P(x + x) with e

p3 : {a : Word, b : Word, c : Word, e0 : a == b, e1 : b == c, p : P(a)} -> P(c)
  let pb = p :: rewrite x in P(x) with e0
  pb :: rewrite x in P(x) with e1


// =============

pa : {lie : {b : Bool} -> b == true} -> Empty
  let e = lie(false) // false == true
  unit :: rewrite x in
    case/Bool x
    | true  => Empty 
    | false => Unit
    : Type
  with e

pb : {b : Bool} -> b == b
  refl(~b)

pc : {lie: {b : Bool} ->  And(b == true, b == false)} -> Empty
  let aux = lie(true) // And(true == true, true == false)
  // true == false
  let aux_left = 
    case/And aux 
    | both => right
    : true == false
  abs_true_false(aux_left)
  
// Dado true == false e um tipo p retorna p 
abs_true_false : {e: true == false} -> Empty
  unit :: rewrite x in 
    case/Bool x
    | true  => Unit 
    | false => Empty
    : Type
  with e

abs_false_true : {e: false == true} -> Empty
  unit :: rewrite x in 
    case/Bool x
    | true  => Empty 
    | false => Unit
    : Type
  with e


pd : {b : Bool} -> Or(b == true, b == false)
  case/Bool b 
  | true  => left(~true == true, ~true == false, refl(~true))
  | false => 
    let p = refl(~b) :: rewrite x in b == x with refl(~false)
    right(~false == true, ~false == false, refl(~false))
  : Or(self == true, self == false)

pe : {b : Bool} -> And(b == b, true == true)
  both(~b == b, ~true == true, refl(~b), refl(~true))

pf : {b : Bool} -> Or(b == b, b == true)
  left(~b == b, ~b == true, refl(~b))

pi : {lie: {a : Bool, b : Bool} -> And(a == b, b == a)} -> Empty
  let aux = lie(false, true)
  let aux_left = 
    case/And aux 
    | both => left
    : false == true
  abs_false_true(aux_left)


pg : {lie: {a : Bool, b : Bool} -> Or(a == true, b == false)} -> Empty
  let aux = lie(false, true)
  let aux_left = 
    case/Or aux 
    | left  => abs_false_true(value)
    | right => abs_true_false(value)
    : Empty
  aux_left

ph: {a : Bool, b : Bool, e : a == b} -> Or(a == true, b == false)
  (case/Bool a 
  | true  => {e2} left(~true == true, ~b == false, refl(~true))
  | false => {e2}
    let pa = refl(~false) :: rewrite x in x == false with e2 // a == false
    let pb = pa :: rewrite x in x == false with e
    right(~false == true, ~b == false, pb)
  : {e2 : self == a} -> Or(self == true, b == false))(refl(~a))

pi : {lie: {a : Bool, b : Bool, e : a == b} -> And(a == true, b == false)} -> Empty
  let aux = lie(true, true, refl(~true)) 
  let aux_left = 
    case/And aux 
    | both => abs_true_false(right)
    : Empty
  aux_left

a_equals_b : {a: Bool, b: Bool, a_is_true: true == a, b_is_true: true == b} -> a == b 
  let bp = refl(~true) :: rewrite x in x == true with a_is_true // a == true
  bp :: rewrite x in a == x with b_is_true