Frex.Lemma

Definitions

record Lemma : Presentation -> Type

  A lemma is an equation that can be proven in the free construction

Totality: total
Visibility: public export
Constructor: 

MkLemma : (equation : Equation (pres .signature)) -> (|-) (QuotientData pres (cast (Fin (equation .support)))) (equation .lhs) (equation .rhs) -> Lemma pres

Projections:

.derivable : ({rec:0} : Lemma pres) -> (|-) (QuotientData pres (cast (Fin ((equation {rec:0}) .support)))) ((equation {rec:0}) .lhs) ((equation {rec:0}) .rhs)

.equation : Lemma pres -> Equation (pres .signature)

.equation : Lemma pres -> Equation (pres .signature)

Visibility: public export

equation : Lemma pres -> Equation (pres .signature)

Visibility: public export

.derivable : ({rec:0} : Lemma pres) -> (|-) (QuotientData pres (cast (Fin ((equation {rec:0}) .support)))) ((equation {rec:0}) .lhs) ((equation {rec:0}) .rhs)

Visibility: public export

derivable : ({rec:0} : Lemma pres) -> (|-) (QuotientData pres (cast (Fin ((equation {rec:0}) .support)))) ((equation {rec:0}) .lhs) ((equation {rec:0}) .rhs)

Visibility: public export

mkLemma : (free : Free pres (cast (Fin n))) -> (eq : (Term (pres .signature) (Fin n), Term (pres .signature) (Fin n))) -> ((free .Data) .Model) .rel (free .Sem (fst eq) (((free .Data) .Env) .H)) (free .Sem (snd eq) (((free .Data) .Env) .H)) => Lemma pres

  Declare a lemma by invoking a free solver on the equation.

Visibility: public export

instantiate : (|-) (QuotientData pres (cast (Fin n))) lhs rhs -> (env : (Fin n -> U a)) -> (|-) a (bindTerm lhs env) (bindTerm rhs env)

  Instantiating a free proof on free terms to get a free proof on a setoid

Visibility: public export

byLemma' : (a : Model pres) -> (lemma : Lemma pres) -> PI ((lemma .equation) .support) Visible (U a) (\env => a .rel (a .Sem ((lemma .equation) .lhs) (\i => index i env)) (a .Sem ((lemma .equation) .rhs) (\i => index i env)))

  Instantiating a lemma to prove a concrete fact in a give model
  The user is expected to pass the instantiation (useful if unification
  is not enough to reconstruct it)

Visibility: public export

byLemma : (a : Model pres) -> (lemma : Lemma pres) -> PI ((lemma .equation) .support) Hidden (U a) (\env => a .rel (a .Sem ((lemma .equation) .lhs) (\i => index i env)) (a .Sem ((lemma .equation) .rhs) (\i => index i env)))

  Instantiating a lemma to prove a concrete fact in a give model
  The user does not have to pass the instantiation (useful if unification
  is enough to reconstruct it)

Visibility: public export