File OpmlPattern

(* From Coq Require Import ssreflect ssrfun ssrbool. *)
From MatchingLogic.OPML Require Export OpmlSignature.
From stdpp Require Export base list list_numbers.
(* This is unset by stdpp. We need to set it again.*)


(* De Bruijn indices for element and set variables*)
Record Edbi := { edbi_n : nat; }.
Record Sdbi := { sdbi_n : nat; }.

Inductive OPMLPattern {Σ : OPMLSignature} :=
| op_upcast
    (from to : opml_sort)
    (subsort : opml_subsort from to)
    (φ : OPMLPattern)
| op_bot (s : opml_sort)
| op_bevar (dbi : Edbi)
| op_bsvar (dbi : Sdbi)
| op_fevar (s : opml_sort) (x : opml_evar s)
| op_fsvar (s : opml_sort) (X : opml_svar s)
| op_imp (φ1 φ2 : OPMLPattern)
| op_app (s : opml_symbol) (args : list OPMLPattern)
| op_ex (s : opml_sort) (φ : OPMLPattern)
| op_mu (s : opml_sort) (φ : OPMLPattern)
.

Fixpoint OPMLPattern_size
    {Σ : OPMLSignature}
    (φ : OPMLPattern)
    : nat :=
match φ with
| op_bot _ ⇒ 1
| op_bevar _ ⇒ 1
| op_bsvar _ ⇒ 1
| op_fevar _ _ ⇒ 1
| op_fsvar _ _ ⇒ 1
| op_imp φ1 φ2 ⇒ 1 + OPMLPattern_size φ1 + OPMLPattern_size φ2
| op_upcast _ _ _ φ' ⇒ 1 + OPMLPattern_size φ'
| op_ex _ φ' ⇒ 1 + OPMLPattern_size φ'
| op_mu _ φ' ⇒ 1 + OPMLPattern_size φ'
| op_app s args ⇒ 1 + sum_list_with OPMLPattern_size args
end.

(* A better induction principle for OPMLPattern *)
Lemma OPMLPattern_deep_ind
    {Σ : OPMLSignature}
    (P : OPMLPattern → Prop)
    (Hupcast :
        ∀
        (from to : opml_sort)
        (subsort : opml_subsort from to)
        (φ : OPMLPattern),
        P φ →
        P (op_upcast from to subsort φ)
    )
    (Hbot :
        ∀ s : opml_sort,
        P (op_bot s)
    )
    (Hbe :
        ∀ dbi : Edbi,
        P (op_bevar dbi)
    )
    (Hbs :
        ∀ dbi : Sdbi,
         P (op_bsvar dbi)
    )
    (Hfe :
        ∀
        (s : opml_sort)
        (x : opml_evar s),
        P (op_fevar s x)
    )
    (Hfs :
        ∀
        (s : opml_sort)
        (X : opml_svar s),
        P (op_fsvar s X)
    )
    (Himp :
        ∀
        φ1 : OPMLPattern,
        P φ1 →
        ∀
        φ2 : OPMLPattern,
        P φ2 → P (op_imp φ1 φ2)
    )
    (Happ :
        ∀
        (s : opml_symbol)
        (args : list OPMLPattern),
        (∀ φ'', φ'' ∈ args → P φ'') →
        P (op_app s args)
    )
    (Hex :
        ∀
        (s : opml_sort)
        (φ : OPMLPattern),
        P φ →
        P (op_ex s φ)
    )
    (Hmu :
        ∀
        (s : opml_sort)
        (φ : OPMLPattern),
        P φ →
        P (op_mu s φ)
    ):
    ∀ φ' : OPMLPattern,
    P φ'
.