File Reshaper

From MatchingLogic Require Export FreshnessManager.
From MatchingLogic.ProofMode Require Export Firstorder.

Import MatchingLogic.Logic.Notations.

Open Scope list_scope. (* needed for mlAssert *)


Section with_signature.
  Context {Σ : Signature}.

  Structure TaggedPattern := TagPattern { untagPattern :> Pattern; }.

  Definition reshape_nil p := TagPattern p.
  Canonical Structure reshape_cons (p : Pattern) : TaggedPattern := reshape_nil p.

  Structure ImpReshapeS (g : Pattern) (l : list Pattern) :=
  ImpReshape
    { irs_flattened :> TaggedPattern ;
      irs_pf : (untagPattern irs_flattened) = foldr patt_imp g l ;
    }.

  Lemma ImpReshape_nil_pf0:
    ∀ (g : Pattern),
      g = foldr patt_imp g [].

  Canonical Structure ImpReshape_nil (g : Pattern) : ImpReshapeS g [] :=
    ImpReshape g [] (reshape_nil g) (ImpReshape_nil_pf0 g).

  Program Canonical Structure ImpReshape_cons
     (g x : Pattern) (xs : list Pattern) (r : ImpReshapeS g xs)
  : ImpReshapeS g (x::xs) :=
    ImpReshape g (x::xs) (reshape_cons (x ---> untagPattern (reshape_cons r))) _.

  Lemma reshape (Γ : Theory) (g : Pattern) (xs: list Pattern) (i : ProofInfo) :
    ∀ (r : ImpReshapeS g xs),
       Γ ⊢i foldr (patt_imp) g xs using i →
       Γ ⊢i (untagPattern (irs_flattened _ _ r)) using i.

  Local Example ex_reshape Γ a b c d:
    well_formed a →
    well_formed b →
    well_formed c →
    well_formed d →
    Γ ⊢i a ---> (b ---> (c ---> d)) using BasicReasoning.

  (*
    Γ ⊢ (φ₁ and ... and φₖ) ---> ψ
    -------------------------------
    Γ ⊢ φ₁ ---> ... ---> φₖ ---> ψ
  *)
  Lemma reshape_lhs_imp_to_and_backward Γ (g x : Pattern) (xs : list Pattern) i :
    well_formed g →
    well_formed x →
    Pattern.wf xs →
    ∀ (r : ImpReshapeS g (x::xs)),
       Γ ⊢i ((foldr (patt_and) x xs) ---> g) using i →
       Γ ⊢i untagPattern (irs_flattened _ _ r) using i .

  Lemma reshape_lhs_imp_to_and_forward' Γ (g x : Pattern) (xs : list Pattern) i :
    well_formed g →
    well_formed x →
    Pattern.wf xs →
    ∀ (r : ImpReshapeS g (x::xs)),
       Γ ⊢i untagPattern (irs_flattened _ _ r) using i →
       Γ ⊢i ((foldr (patt_and) x xs) ---> g) using i.

  (*
      Γ ⊢ φ₁ ---> ... ---> φₖ ---> ψ
      ------------------------------
      Γ ⊢ (φ₁ and ... and φₖ) ---> ψ
  *)
  Lemma reshape_lhs_imp_to_and_forward Γ (g x : Pattern) (xs : list Pattern) i :
    well_formed g →
    well_formed x →
    Pattern.wf xs →
    ∀ (r : ImpReshapeS g (x::xs)),
       Γ ⊢i untagPattern (irs_flattened _ _ r) using i →
       match (rev xs) with
       | [] ⇒ Γ ⊢i x ---> g using i
       | yk::ys ⇒
          Γ ⊢i ((foldr (patt_and) yk (x::(rev ys))) ---> g) using i
       end.

  Local Example ex_match_imp Γ a b c d:
    well_formed a →
    well_formed b →
    well_formed c →
    well_formed d →
    Γ ⊢i c ---> (b ---> (a ---> d)) using BasicReasoning →
    Γ ⊢i a ---> (b ---> (c ---> d)) using BasicReasoning.

  Structure AndReshapeS (g : Pattern) (l : list Pattern) :=
  AndReshape
    { ars_flattened :> TaggedPattern ;
      ars_pf : (untagPattern ars_flattened) = foldr patt_and g l ;
    }.

  Lemma AndReshape_nil_pf0:
    ∀ (g : Pattern),
      g = foldr patt_and g [].

  Canonical Structure AndReshape_nil (g : Pattern) : AndReshapeS g [] :=
    AndReshape g [] (reshape_nil g) (AndReshape_nil_pf0 g).

  Program Canonical Structure AndReshape_cons
     (g x : Pattern) (xs : list Pattern) (r : AndReshapeS g xs)
  : AndReshapeS g (x::xs) :=
    AndReshape g (x::xs) (reshape_cons (x and untagPattern (reshape_cons r))) _.

  Lemma reshape_and (Γ : Theory) (g : Pattern) (xs: list Pattern) (i : ProofInfo) :
    ∀ (r : AndReshapeS g xs),
       Γ ⊢i foldr (patt_and) g xs using i →
       Γ ⊢i (untagPattern (ars_flattened _ _ r)) using i.

  Local Example ex_reshape_and Γ a b c d:
  well_formed a →
  well_formed b →
  well_formed c →
  well_formed d →
  Γ ⊢i a and b and c and d using BasicReasoning.

    (*
      Γ ⊢ φ₁ ---> ... ---> φₖ ---> ψ
      ------------------------------
      Γ ⊢ (φ₁ and ... and φₖ) ---> ψ
    *)
  Lemma reshape_lhs_and_to_imp_backward Γ (g x : Pattern) (xs : list Pattern) i :
    well_formed g →
    well_formed x →
    Pattern.wf xs →
    ∀ (r : AndReshapeS x xs),
       Γ ⊢i ((foldr (patt_imp) g (x::xs))) using i →
       Γ ⊢i (untagPattern (ars_flattened _ _ r)) ---> g using i .

  Lemma reshape_lhs_and_to_imp_forward Γ (g x : Pattern) (xs : list Pattern) i :
    well_formed g →
    well_formed x →
    Pattern.wf xs →
    ∀ (r : AndReshapeS x xs),
      Γ ⊢i (untagPattern (ars_flattened _ _ r)) ---> g using i →
      Γ ⊢i ((foldr (patt_imp) g (x::xs))) using i.

  Local Example ex_match_and Γ a b c d:
   well_formed a →
   well_formed b →
   well_formed c →
   well_formed d →
   Γ ⊢i (a and b and c) ---> d using BasicReasoning.

End with_signature.