File tutorial

(* What follows is a minimal example of how to use the ProofMode. *)

From MatchingLogic Require Import ProofMode.MLPM
                                  Definedness_ProofSystem.

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


Open Scope string_scope.
Open Scope list_scope.

Section tutorial.

Context {Σ : Signature}
        {Γ : Theory}
        (ϕ : Pattern)
        (wfϕ : well_formed ϕ).

(* Below we prove that in matching logic, ϕ -> ϕ for any pattern ϕ. *)
Example phi_implies_phi :
    Γ ⊢ ϕ ---> ϕ.

(* We can also work with conjunction and disjunction. *)

Context (ϕ₁ : Pattern)
        (wfϕ₁ : well_formed ϕ₁)
        (ϕ₂ : Pattern)
        (wfϕ₂ : well_formed ϕ₂).

Example and_or :
    Γ ⊢ ϕ₁ and ϕ₂ ---> ϕ₁ or ϕ₂
.

Context (ϕ₃ : Pattern)
        (wfϕ₃ : well_formed ϕ₃)
        (ϕ₄ : Pattern)
        (wfϕ₄ : well_formed ϕ₄).

Example use_rewrite :
    Γ ⊢ ϕ₁ <---> ϕ₂ →
    (* The ⋅ operator is an application. *)
    Γ ⊢ (ϕ₃ ⋅ ϕ₁ ⋅ ϕ₄) <---> (ϕ₃ ⋅ ϕ₂ ⋅ ϕ₄)
.

(* We can also use definedness and equality.
   To do so, we have to assume that the signature contains a definedness symbol,
   and the theory a definedness axiom.
   Otherwise, the signature and axiom can be arbitrary.
*)

(* Obviously, without the definedness symbol, we cannot use equality. *)

(* The typeclass Definedness_Syntax.Syntax ensures the presence of the definedness symbol
   in the (implicit) signature Σ.
 *)
Context {syntax : Definedness_Syntax.Syntax}.

Example use_rewriteBy :
    Γ ⊢ (ϕ₁ ⋅ ϕ₄ =ml ϕ₂ ⋅ ϕ₄) ---> (ϕ₁ =ml ϕ₂) ---> ((ϕ₃ ⋅ (ϕ₁ ⋅ ϕ₄)) <---> (ϕ₃ ⋅ (ϕ₂ ⋅ ϕ₄)))
.

Context {HΓ : Definedness_Syntax.theory ⊆ Γ}.

Example use_rewriteBy :
    Γ ⊢ (ϕ₁ ⋅ ϕ₄ =ml ϕ₂ ⋅ ϕ₄ ) ---> (ϕ₁ =ml ϕ₂) ---> ((ϕ₃ ⋅ (ϕ₁ ⋅ ϕ₄)) <---> (ϕ₃ ⋅ (ϕ₂ ⋅ ϕ₄)))
.

(*
   We now demonstrate how to use local hypotheses that are implications.
*)
Example use_mlApply :
    Γ ⊢ (ϕ₁ ---> ϕ₂ ⋅ ϕ₃) ---> (ϕ₂ ⋅ ϕ₃ ---> ϕ₃) ---> (ϕ₁ ---> ϕ₃).

Context (ψ : Pattern)
        (wfψ : well_formed (ex, ψ)).

(*
   What if we have a matching logic implication in a Coq hypothesis
   or in a lemma? There is `mlApplyMeta` for that.
*)
Example use_mlApplyMeta :
    Γ ⊢ ϕ₁ ---> ((ex, ψ) ⋅ ϕ₂) ---> ϕ₃ ---> (ex, (ψ ⋅ ϕ₂)).
    Check Prop_ex_left.
    (*
        Prop_ex_left
        : ∀ (Γ : Theory) (ϕ ψ : Pattern),
            well_formed (ex , ϕ)
            → well_formed ψ
            → Γ ⊢i (ex , ϕ) ⋅ ψ ---> (ex , ϕ ⋅ ψ) using BasicReasoning
    *)
    (* Did you notice that mlApplyMeta automatically instantiated
       all the preconditions of the lemma?
       That is, without some magic happening on the background,
       one would need to manualy specify them,
       and solve the well-formedness subgoals.
    *)
Defined.

End tutorial.