File Revert_size

From MatchingLogic Require Import Theories.Definedness_Syntax
                                  ProofMode.MLPM.

Import MatchingLogic.Logic.Notations.


Local Lemma Private_revert_forall_iter {Σ : Signature} (Γ : Theory) :
  ∀ (l : list Pattern) (ϕ : Pattern) x,
  Pattern.wf l →
  well_formed ϕ →
  Γ ⊢i foldr patt_imp (all , ϕ^{{evar: x ↦ 0}}) l ---> foldr patt_imp ϕ l
    using BasicReasoning.

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 X := patt_free_evar "X".
  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 :=
    sym_zero.
  Definition B : Pattern :=
    patt_app sym_succ sym_zero.

Definition private_test_revert_1 :=
  (Private_revert_forall_iter ∅ [] patt_bott (fresh_evar patt_bott)
    ltac:(wf_auto2) ltac:(wf_auto2)).
Definition private_test_revert_2 :=
  (revert_forall_iter ∅ [] patt_bott (fresh_evar patt_bott)
    ltac:(wf_auto2) ltac:(wf_auto2)).
Definition private_test_revert_3 :=
  (Private_revert_forall_iter ∅ [A;B;A;B;A;B] patt_bott (fresh_evar patt_bott)
    ltac:(wf_auto2) ltac:(wf_auto2)).
Definition private_test_revert_4 :=
  (revert_forall_iter ∅ [A;B;A;B;A;B] patt_bott (fresh_evar patt_bott)
    ltac:(wf_auto2) ltac:(wf_auto2)).

    (*
  Compute proof_size_info (ex1_low ∅ A B ltac:(wf_auto2) ltac:(wf_auto2)).
  Compute proof_size_info (ex1_pm ∅ A B ltac:(wf_auto2) ltac:(wf_auto2)). *)

End compute.