namespace http://cds.omdoc.org/urtheories❚

import rules scala://quotation.mmt.kwarc.info❚

/T   higher-order logic with quotation and evaluation, mostly following Bill Farmer's work ❚
theory HOLQE : ?LF =
   # Higher-order logic❙
  
   ## Types❙

   /T the LF-type representing HOL types ❙ 
   tp  : type❙
   /T function types ❙ 
   fun : tp ⟶ tp ⟶ tp❘ # 1 ⇒ 2 prec 20❙

   /T Normally we represent object language variables using LF variables, in which case the following is redundant.
      But Farmer's language follows the traditional style of assuming an infinite supply of variables at every type.
      It is critical to capture this in the representation because he allows quoting terms with free variables.❙
   /T the type of variables at a given HOL type❙
   Var : tp ⟶ type❙
   /T the constructor for concrete variables %x:a at a given HOL type where x is any identifier that is parsed as a closed term
      Most of the time, we do not need this because we can use LF-variables v:Var a as meta-variables that range over HOL variables at type a.❙ 
   var # % L1T prec 200❙
   /T the typing rule (%x:a):Var a for concrete variables cannot be expressed in LF, so we implement an MMT rule❙ 
   rule rules?ConcreteVariable❙
   
   ## Terms❙
   
   /T the LF-type representing HOL terms of a given HOL type ❙  
   tm : tp ⟶ type❘ # tm 1 prec -1❙
   /T all variables are terms of their respective type ❙ 
   tvar : {a} Var a ⟶ tm a❘# tvar 2❘## 2 prec 100❙
   /T λ-abstraction (contrary to typical LF-encodings, we bind explicit variables that have to be injected into terms using tvar ❙ 
   lam : {a, b} (Var a ⟶ tm b) ⟶ tm a ⇒ b❘ # λ 3❙
   /T application ❙ 
   app : {a, b} tm a ⇒ b ⟶ tm a ⟶ tm b❘ # 3 @ 4 prec 20❙
   /T undefined terms (not needed here, but probably needed later on when evaluating quotations of ill-typed terms❙ 
   undefined : {a} tm a❘# ⊥ 1❙

   /T booleans, connectives, and proofs❙ 
   bool : tp❙
   equal : {a} tm a ⟶ tm a ⟶ tm bool ❘ # 2 = 3 prec 10❙

   ded  : tm bool ⟶ type❘ # ⊦ 1 prec -1❙
   
   # Quotation❙ 
   
   /T We add HOL types that reify HOL concepts❙ 

   ## Quoting Terms❙ 

   /T We add a type holding quotations of HOL terms. All terms may be quoted, including ill-typed ones.
      Effectively, this amounts to having a type that represents the untype λ-calculus inside a typed λ-calculus.❙ 

   ### Syntax❙    
      
   /T the type of quoted terms❙
   qtp  : tp ❘ # ε❙
   /T quoted variables❙
   qvar : {a} Var a ⟶ tm ε❘# qvar 2 prec 100❘## qvar 2 prec 100 ❙
   /T quoted λ-abstractions❙
   qlam : {a} Var a ⟶ tm ε ⟶ tm ε ❘ # qlam 2 . 3 prec 150❙
   /T quoted applications❙
   qapp : tm ε ⟶ tm ε ⟶ tm ε ❘ # qapp 1 2 prec 20❙
   /T quoted quotations❙
   qquote: tm ε ⟶ tm ε❙

   /T Finally, we add a meta-level operation that turns a term into the corresponding quotation.
      We may think of it as having type ${a}tm a ⟶ tm ε$ except. However, quotation may not be subject to congruence and therefore cannot have an LF type.❙   
   quote # ⌜ 1 ⌝  prec 10❙
   /T the rule that eliminates occurrences of quote by constructing the corresponding term of type $tm ε$
      HOL variables in the argument are quoted using $qvar$, LF variables remain, which gives rise to quasi-quotation.❙ 
   rule rules?QuoteTerm❙

   ### Semantics❙

   /T the predicate expressing that a term is the quotation of a term of a given types.❙
   oftype     : tm ε ⟶ tp ⟶ tm bool❘# 1 $ 2 prec 5❙
   /T typing rule for quoted variables❙
   oftype_var : {a,v: Var a} ⊦ qvar v $ a❙
   /T typing rule for quoted λ-abstractions❙
   oftype_lam : {a,b,v:Var a,E} ⊦ E $ b ⟶ ⊦ qlam v.E $ a ⇒ b❙
   /T typing rule for quoted applications❙
   oftype_app : {a,b,F,E} ⊦ F $ a ⇒ b ⟶ ⊦ E $ a ⟶ ⊦ qapp F E $ a ⇒ b❙
   /T typing rule for quoted quotations❙
   oftype_quote: {E,a} ⊦ E $ a ⟶ ⊦ qquote E $ ε❙   

   ## Quoting Substitutions❙ 

   /T Expanding on Farmer's work, we also add a type holding HOL substitutions.
      Effectively, this amounts to a language with explicit substitutions.
      Because all variables are always in scope, every substitution maps all variables to terms.❙ 

   ### Syntax❙
   
   /T the type of substitutions❙
   stp  : tp❘ # sub❙
   /T the identity substitutions❙
   idsub: tm sub❙
   /T the substitution that modifies a given substitution in one place❙
   update: {a} tm sub ⟶ Var a ⟶ tm a ⟶ tm sub ❘# 2 + 3 ↦ 4 prec 50❙

   /T abbreviation for the substitution that maps one variable❙   
   singlesub: {a} Var a ⟶ tm a ⟶ tm sub ❘# 2 ↦ 3 prec 51❘
            = [a,v,t] idsub + v ↦ t❙

   /T Finally, we add a meta-level operation that turns a substitution into the corresponding quotation.❙   
   subs # ` L1T,… ´  prec 10❙
   /T the rule that eliminates occurrences of subs by constructing the corresponding term of type $tm sub$❙ 
   // rule rules?QuoteSubs❙

   ### Semantics❙

   /T an auxiliary predicate to reason about inequality of variables❙
   diff : {a,b} Var a ⟶ Var b ⟶ tm bool ❘# 3 ≠ 4 prec 10❙ // notation parsing errors not reported correctly? ❙
   
   /T the function that retrieves the map of a variable by a substitution❙
   lookup: {a} tm sub ⟶ Var a ⟶ tm a ❘# 3 ' 2 prec 15❙
   /T the lookup rule for the identity substitution❙   
   subst_id     : {a,v: Var a} ⊦ v'idsub = (tvar v)❙
   /T the lookup rule for an update to the needed variables❙   
   subst_update_same : {s,a, v: Var a, E} ⊦ v'(s+v↦E) = E❙
   /T the lookup rule for an update to some other variable❙   
   subst_update_diff : {s,a,b, v: Var a, w: Var b, E} ⊦ v ≠ w ⟶ ⊦ v'(s+w↦E) = v's❙
   
   # Evaluation❙
   
   /T Evaluation internalizes the model-theoretical semantics: evaluation takes a term and a substitution (which provides the assignment to the free variables) and returns its interpretation in the model.
   
   Evaluation is only defined for quotations of well-typed terms. Because the type of a quotation is not stored in the quotation,
   * evaluation takes a HOL-type as an additional argument,
   * evaluation rules take typing assumptions.❙
   
   /T the evaluation operator❙
   eval     : {a} tm ε ⟶ tm sub ⟶ tm a ❘ # ⟦ 2 $ 1 ⟧ 3 prec -5 ❘ ## ⟦ 2 $ 1 ⟧ ^ 3 prec -5❙
   /T the evaluation rule for variables: apply the assignment❙
   eval_var : {a, v: Var a, s} ⊦ (⟦qvar v $ a⟧s) = v's❙
   /T the evaluation rule for λ-abstractions qlam v.E: build the function that maps x to the evaluation of E under the assignment of v to x❙
   eval_fun : {a, b, v: Var a, E, s} ⊦ E $ b ⟶ ⊦ (⟦qlam v.E $ a ⇒ b⟧s) = λ[x](⟦E $ b⟧ s + v ↦ tvar x)❙
   /T the evaluation rule for applications: straightforward❙
   eval_app : {a,b, F, X, s} ⊦ F $ a ⇒ b  ⟶  ⊦ X $ a  ⟶  ⊦ (⟦qapp F X $ b⟧s) = (⟦F $ a ⇒ b⟧s) @ ⟦X $ a⟧s❙
   /T the evaluation rule for quotations: evaluation cancels quotation❙
   eval_quote : {X, s} ⊦ X $ ε  ⟶  ⊦ (⟦qquote X $ ε⟧s) = X❙
❚
  
/T Now we formalize two challenge problems posed by Farmer❚
 
theory ExcludedMiddle : ?HOLQE =
  not : tm bool ⟶ tm bool❘# ¬ 1❙
  or  : tm bool ⟶ tm bool ⟶ tm bool❘# 1 ∨ 2❙
  em  : {f,s} ⊦ f $ bool ⟶ ⊦ (⟦f$bool⟧s) ∨ ¬ ⟦f$bool⟧s ❙
❚

theory PolyDiff : ?HOLQE =
  /T real numbers and derivatives❙
  R: tp❙
  derivative : tm R ⇒ R ⟶ tm R ⇒ R❙
  
  /T a transformer that computes the derivative of a polynomial and its meaning formula❙
  ispolyin: tm ε ⟶ Var R ⟶ tm bool❙
  polyderiv: tm ε ⟶ Var R ⟶ tm ε❙
  meaning: {v, p} ⊦ ispolyin p v ⟶ ⊦ derivative (λ[x] ⟦p $ R⟧v ↦ tvar x) = (λ[x] ⟦polyderiv p v $ R⟧v ↦ tvar x) ❙
❚