implicationallogic.agda

module implicationallogic where

module Example where

  postulate
    Person        : Set
    john          : Person
    mary          : Person
    IsStudent     : Person → Set
    maryIsStudent : IsStudent mary
    implication   : IsStudent mary → IsStudent john

  Lemma₁ : Set
  Lemma₁ = IsStudent john

  proof-lemma₁ : Lemma₁
  proof-lemma₁ = {!!}

  postulate
    barbara : Person

  -- gets a proof of john is a student and
  -- returns a proof of barbara is a student
  Lemma₂ : Set
  Lemma₂ = IsStudent john → IsStudent barbara

  proof-lemma₂ : Lemma₂
  proof-lemma₂ = {!!}



module Example₂ where

  postulate
    A : Set
    B : Set

  -- We can introduce the formula (or set) expressing A → (A → B) → B
  -- as follows:
  Lemma₁ : Set
  Lemma₁ = A → (A → B) → B

  -- When the type of goal is an implication, it is usually shown
  -- by λ-abstraction from the premises of the implication.
  lemma₁′ : Lemma₁
  lemma₁′ = {!!}

  -- Instead of introducing a λ-abstraction, we apply lemma₁ to variables
  -- a (of type A) and a-b (of type A → B).
  lemma₁ : Lemma₁
  lemma₁ a a-b = {!!} -- to show the context, type: C-c C-,



module TerminationChecker where

  postulate
    A : Set
    B : Set

  a : A
  a = a

  -- $ agda implicationallogic.agda
  -- $ agda --safe -i . -i ~/build/agda-stdlib-0.8/src/ implicationallogic.agda
  -- '--safe' disable postulates, unsafe OPTION pragmas and primTrustMe

  f : A → A
  f a = a

  lemma : (A → B) → A → B
  lemma a-b a = lemma a-b a