File Complex

From MatchingLogic Require Import Theories.Definedness_ProofSystem.

Import MatchingLogic.Logic.Notations
       MatchingLogic.Theories.Definedness_Syntax.Notations.


Section running.
  Notation definedness_theory := Theories.Definedness_Syntax.theory.
  Notation definedness_syntax := Theories.Definedness_Syntax.Syntax.
  Context
    {Σ : Signature}
    {defsyntax : definedness_syntax}
    (Γ : Theory)
    (HΓ : Theories.Definedness_Syntax.theory ⊆ Γ).

  Lemma running
    (x : evar)
    (f ϕ₁ ϕ₂ : Pattern)
    :
    mu_free f →
    well_formed f →
    well_formed (ex, ϕ₁) →
    well_formed (ex, ϕ₂) →
    Γ ⊢ (((all, (ϕ₂ =ml ϕ₁)) and (f ⋅ (evar_open x 0 ϕ₁))) --->
        ex, (f ⋅ ϕ₂))
  .

  Lemma running_functional_subst (φ φ' : Pattern) :
    mu_free φ → well_formed φ' → well_formed_closed_ex_aux φ 1 →
    well_formed_closed_mu_aux φ 0 →
    Γ ⊢i φ^[evar:0↦φ'] and (ex , φ' =ml b0) ---> (ex , φ)
              using AnyReasoning.

  Lemma running_forall_functional_subst (φ φ' : Pattern) :
    mu_free φ → well_formed φ' → well_formed_closed_ex_aux φ 1 →
    well_formed_closed_mu_aux φ 0 →
    Γ ⊢i (all , φ) and (ex , φ' =ml b0) ---> φ^[evar:0↦φ']
              using AnyReasoning.

  Local Lemma lhs_from_and_low:
    ∀ (a b c : Pattern) (i : ProofInfo),
    well_formed a
      → well_formed b
        → well_formed c
          → Γ ⊢i a ---> b ---> c using i → Γ ⊢i a and b ---> c using i.

  Lemma running_low
    (x : evar)
    (f ϕ₁ ϕ₂ : Pattern)
    :
    mu_free f →
    well_formed f →
    well_formed (ex, ϕ₁) →
    well_formed (ex, ϕ₂) →
    Γ ⊢ (((all, (ϕ₂ =ml ϕ₁)) and (f ⋅ (evar_open x 0 ϕ₁))) --->
        ex, (f ⋅ ϕ₂))
  .

End running.

Section compute.

  Inductive Symbols :=
  | sym_import_definedness (d : Definedness_Syntax.Symbols)
  | Zero | Succ (* constructors for Nats *)
  | TT | FF
  | even
  .

  Instance Symbols_eqdec : EqDecision Symbols.

  #[local]
  Program Instance Symbols_fin : Finite Symbols :=
  {|
    enum := [Zero; Succ; TT ; FF; even;
    sym_import_definedness Definedness_Syntax.def_sym] ;
  |}.

  Instance signature : Signature :=
  {| variables := StringMLVariables ;
    ml_symbols := {|
      symbols := Symbols ;
    |}
  |}.

  Instance definedness_syntax : Definedness_Syntax.Syntax :=
  {|
    Definedness_Syntax.sym_inj := sym_import_definedness;
  |}.

  Open Scope string_scope.
  Let X0 := patt_free_evar "X0".
  Let Y := patt_free_evar "Y".
  Let sym_even := patt_sym even.
  Let sym_succ := patt_sym Succ.
  Let sym_zero := patt_sym Zero.
  Let sym_tt := patt_sym TT.
  Let sym_ff := patt_sym FF.
  (* axioms *)
  Definition defined : Pattern := Definedness_Syntax.axiom AxDefinedness.

  Definition A : Pattern := patt_bound_evar 0.
  Definition B : Pattern := patt_app sym_succ Y.

  (*
    (∀z. S y = z) ∧ even x ---> ∃z. even (S y)
  *)
  Definition proof_running_low :=
    running_low theory ltac:(set_solver) "X"
    sym_even A B
    ltac:(auto) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2).
  Definition proof_running_pm :=
    running theory ltac:(set_solver) "X"
    sym_even A B
    ltac:(auto) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2).

End compute.