File Rewrite

From MatchingLogic Require Import Theories.Definedness_Syntax
                                  ProofMode.MLPM.

Import MatchingLogic.Logic.Notations.


Fixpoint proof_size {Σ : Signature} {φ : Pattern} {Γ}
   (pf : ML_proof_system Γ φ) : nat :=
match pf with
 | ML_Modus_ponens _ phi1 phi2 x x0 ⇒ 1 + proof_size x + proof_size x0
 | ML_Ex_gen _ phi1 phi2 x x0 x1 x2 x3 ⇒ 1 + proof_size x2
 | ML_Framing_left _ phi1 phi2 psi x x0 ⇒ 1 + proof_size x0
 | ML_Framing_right _ phi1 phi2 psi x x0 ⇒ 1 + proof_size x0
 | ML_Svar_subst _ phi psi X x x0 x1 ⇒ 1 + proof_size x1
 | ML_Knaster_tarski _ phi psi x x0 ⇒ 1 + proof_size x0
 | ML_Existence _ ⇒ 1
 | _ ⇒ 1
end.

Definition proof_size_info {Σ : Signature} {φ Γ i} (pf : derives_using Γ φ i) : nat :=
match pf with
 | exist _ x x0 ⇒ proof_size x
end.

Lemma ex2_low {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
  well_formed (A ---> B ---> C ---> D) = true →
  Γ ⊢ ((B ⋅ C) <---> D) →
  Γ ⊢ ((A ⋅ (B ⋅ C)) ---> (A ⋅ D)).

Lemma ex2_low2 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
  well_formed (A ---> B ---> C ---> D) = true →
  Γ ⊢ ((B ⋅ C) <---> D) →
  Γ ⊢ ((A ⋅ (B ⋅ C)) ---> (A ⋅ D)).

Lemma ex2_low3 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
  well_formed (A ---> B ---> C ---> D) = true →
  Γ ⊢ ((B ⋅ C) <---> D) →
  Γ ⊢ ((A ⋅ (B ⋅ C)) ---> (A ⋅ D)).

Lemma ex2_low4 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
  well_formed (A ---> B ---> C ---> D) = true →
  Γ ⊢ ((B ⋅ C) <---> D) →
  Γ ⊢ ((A ⋅ (B ⋅ C)) ---> (A ⋅ D)).

Lemma ex2_pm {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
  well_formed (A ---> B ---> C ---> D) = true →
  Γ ⊢ ((B ⋅ C) <---> D) →
  Γ ⊢ ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.

Lemma ex2_coq {T : Type} A (B : T → Prop) C D:
  B C ↔ D →
  A (B C) → A D.

Lemma ex2_pm2 {Σ : Signature} (A B C D : Pattern) (Γ : Theory) :
  well_formed (A ---> B ---> C ---> D) = true →
  Γ ⊢ ((B ⋅ C) <---> D) →
  Γ ⊢ ((A ⋅ (B ⋅ C)) ---> (A ⋅ D))
.

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;
    |}.

  Let Z := patt_free_evar "Z".
  Let X := patt_free_evar "X".
  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.

(*   Lemma functional_syms :
    theory ⊢ patt_exists (patt_app sym_succ sym_zero =ml b0).
  Proof.
    subst sym_succ sym_zero.
    unfold patt_equal, patt_total, patt_iff, patt_and.
    Search derives_using patt_exists  patt_defined.
    Search patt_defined patt_total.
    Search patt_imp patt_and. (* 
    pose proof (nimpl_eq_and theory (patt_sym Succ ⋅ patt_sym Zero) b0).
     at 1.
    Search derives_using patt_exists. *)
    eapply MP. instantiate (1 := (ex , patt_sym Succ ⋅ patt_sym Zero =ml b0) ^ X).
    2: gapply Ex_quan.
    2-3: shelve.
    unfold instantiate. mlSimpl. simpl.
    
    Search patt_equal derives_using.
    Search patt_free_evar derives_using.
    unfold patt_equal, patt_total, patt_iff, patt_and.
    Search patt_defined patt_or.
    remember (@patt_sym signature Succ ⋅ @patt_sym signature Zero) as A.
    epose proof (nimpl_eq_and theory A X _ _).
    apply useAnyReasoning in H.
    epose proof (not_not_eq theory (! (A ---> X) or ! (X ---> A)) _).
    apply useAnyReasoning in H0.
    mlRewrite H0 at 1. clear H0.
    mlRewrite H at 1.
  Defined. *)

(*   Definition proof2_low : nat := proof_size_info (ex2_low sym_succ sym_succ sym_zero X ∅ ltac:(wf_auto2)).
  Definition proof2_pm : nat := proof_size_info (ex2_low2 ∅ A B ltac:(wf_auto2) ltac:(wf_auto2)).
  Definition proof2_pm2 : nat := proof_size_info (ex2_pm ∅ A B ltac:(wf_auto2) ltac:(wf_auto2)). *)

  Lemma premise :
    ∅ ⊢ Y ⋅ Z <---> Y ⋅ Z.

  Definition proof2_low := ex2_low X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise.
  Definition proof2_pm := ex2_low2 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise.
  Definition proof2_pm2 := ex2_pm X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise.
  Definition proof2_pm3 := ex2_pm2 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise.

  Definition proof2_low3 := ex2_low3 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise.
  Definition proof2_low4 := ex2_low4 X Y Z (Y ⋅ Z) ∅ ltac:(wf_auto2) premise.

(* 
  Compute proof_size_info (ex2_low ∅ A B ltac:(wf_auto2) ltac:(wf_auto2)).
  Compute proof_size_info (ex2_pm ∅ A B ltac:(wf_auto2) ltac:(wf_auto2)). *)

End compute.