File ProofModePattern
From Equations Require Import Equations.
From MatchingLogic Require Export
Signature
Pattern
.
From stdpp Require Export
strings
stringmap
.
Require Import String.
Equations? list_map_pfin
{A B : Type}
(l : list A)
(f : ∀ (x : A) (pf: x ∈ l), B)
: list B :=
list_map_pfin [] _ := [] ;
list_map_pfin (x::xs) f := (f x _)::(list_map_pfin xs (fun x H ⇒ f x _)) .
Lemma list_map_pfin_spec {A B : Type} (f : A → B) (l : list A) :
list_map_pfin l (fun (x : A) (_ : x ∈ l) ⇒ f x) = List.map f l.
Lemma length_list_map_pfin
{A B : Type}
(l : list A)
(f : ∀ (x : A) (pf: x ∈ l), B)
:
List.length (list_map_pfin l f) = List.length l
.
Definition VarName := string.
Definition EVarName := VarName.
Definition SVarName := VarName.
Definition incr_values
(vm : gmap VarName nat)
: gmap VarName nat
:= fmap (fun n ⇒ S n) vm.
(*
Represents a context in which a pattern is well-defined.
In particular, `pc_evm` is the set of element variables in context.
*)
Record PContext := mkPContext {
pc_evm : gmap EVarName nat ;
pc_svm : gmap SVarName nat ;
}.
(*Compute (fresh_string "X" (<"X" := 1>∅)).*)
Definition this_or_fresh
(this : VarName)
(g : gmap VarName nat)
: VarName
:=
fresh_string this g
.
Lemma this_or_fresh_fresh this g:
g !! (this_or_fresh this g) = None.
Definition renaming_function
(new_key old_key some_key : VarName) : VarName :=
match (decide (some_key = old_key)) with
| left _ ⇒ new_key
| right _ ⇒
match (decide (some_key = new_key)) with
| left _ ⇒ old_key
| right _ ⇒ some_key
end
end.
#[global]
Instance renaming_function_injective new_name old_name:
Inj eq eq (renaming_function new_name old_name).
Definition update_key
(new_key old_key : VarName)
(m : gmap VarName nat)
: gmap VarName nat
:= kmap (renaming_function new_key old_key) m
.
Definition update_evm_key
(new_key old_key : EVarName)
(pctx : PContext)
: PContext
:= mkPContext
(update_key new_key old_key (pc_evm pctx))
(pc_svm pctx)
.
Definition update_svm_key
(new_key old_key : SVarName)
(pctx : PContext)
: PContext
:= mkPContext
(pc_evm pctx)
(update_key new_key old_key (pc_svm pctx))
.
Definition max_value (d : nat) (m : gmap VarName nat) : nat :=
map_fold (fun k v r ⇒ Nat.max v r) d m
.
Lemma max_value_kmap (f : VarName → VarName) {injF : Inj eq eq f} (d : nat) (m : gmap VarName nat):
max_value d (kmap f m) = max_value d m
.
Lemma max_value_in_leq
(m : gmap VarName nat)
(d : nat)
(name : VarName)
:
m !! name = Some d →
d ≤ max_value 0 m
.
Definition boundary_value (m : gmap VarName nat) : nat :=
match (decide (m = ∅)) with
| left _ ⇒ 0
| right _ ⇒ S (max_value 0 m)
end
.
Definition pc_add_ename
(ctx : PContext)
(name : EVarName) :=
mkPContext ((<[name := 0]>(incr_values (pc_evm ctx)))) (pc_svm ctx)
.
Definition pc_add_sname
(ctx : PContext)
(name : SVarName) :=
mkPContext (pc_evm ctx) ((<[name := 0]>(incr_values (pc_svm ctx))))
.
Record Pattern_in_context
{Σ : Signature} := mkPIC {
pic_pic: PContext → Pattern;
pic_wf : ∀ (pc : PContext),
let phi := pic_pic pc in
well_formed_positive phi ∧ (* TODO no_negative, no_positive_occurrence*)
well_formed_closed_ex_aux phi (boundary_value (pc_evm pc)) ∧
well_formed_closed_mu_aux phi (boundary_value (pc_svm pc)) ;
}
.
(*
So what notations we want to support?
¬ϕ ≡ ϕ ---> ⊥
ϕ₁ \/ ϕ₂ ≡ ¬ϕ₁ ---> ϕ₂
∀ x. ϕ ≡ ¬ ∃ x. ¬ ϕ
So, a notation is parametric in
(1) how many patterns it takes as an argument.
(2) how many element variables it binds
(3) how many set variables it binds.
*)
Record MLConstruct
(mlc_arity : nat)
(mlc_ebinder_arity : nat)
(mlc_sbinder_arity : nat)
{Σ : Signature} := {
(*mlc_level : nat ;*)
mlc_expand :
list Pattern_in_context → (* patterns *)
list EVarName → (* bound evars*)
list SVarName → (* bound svars*)
option Pattern_in_context ;
mlc_expand_almost_total :
∀
(args : list Pattern_in_context)
(ebinders : list EVarName)
(sbinders : list SVarName),
List.length args = mlc_arity →
List.length ebinders = mlc_ebinder_arity →
List.length sbinders = mlc_sbinder_arity →
∃ ϕ_in_context,
mlc_expand args ebinders sbinders = Some ϕ_in_context ;
}.
Section sec.
Context
{Σ : Signature}
.
Inductive PMPattern : Set :=
| pmpatt_inj (ln : Pattern) (wfpf : Pattern.well_formed ln)
| pmpatt_construct
{a ea sa : nat}
(construct : MLConstruct a ea sa)
(args : vec PMPattern a)
(bound_evars : vec EVarName ea)
(bound_svars : vec SVarName sa)
.
Equations PMPattern_size
(ϕ : PMPattern)
: nat := {
PMPattern_size (pmpatt_inj _ _) := 1 ;
PMPattern_size (pmpatt_construct _ args _ _) :=
S (@PMPattern_size_vec _ args)
where PMPattern_size_vec
{arity : nat}
(v : vec PMPattern arity)
: nat := {
@PMPattern_size_vec _ vnil := 1 ;
@PMPattern_size_vec _ (vcons x xs) :=
(PMPattern_size x + PMPattern_size_vec xs)
}
}
.
Lemma PMPattern_size_clause_2_PMPattern_size_vec_spec
(ar1 ea1 sa1 : nat) (con : MLConstruct ar1 ea1 sa1) a e s ar args':
@PMPattern_size_clause_2_PMPattern_size_vec PMPattern_size ar1 ea1 sa1 con a e s ar args'
= S (list_sum (fmap (fun p ⇒ PMPattern_size p) (vec_to_list args')))
.
Equations eq_apply_4
{T1 T2 T3 T4 R : Type}
(f: T1 → T2 → T3 → T4 → R)
(arg1 : T1)
(arg2 : T2)
(arg3 : T3)
(arg4 : T4)
:
{r : R & r = f arg1 arg2 arg3 arg4} :=
eq_apply_4 f arg1 arg2 arg3 arg4
:= existT (f arg1 arg2 arg3 arg4) (@eq_refl _ _) .
Definition eq_apply_5
{T1 T2 T3 T4 T5 R : Type}
(f: T1 → T2 → T3 → T4 → T5 → R)
(arg1 : T1)
(arg2 : T2)
(arg3 : T3)
(arg4 : T4)
(arg5 : T5)
:
{r : R & r = f arg1 arg2 arg3 arg4 arg5}
.
Definition eq_apply_7
{T1 T2 T3 T4 T5 T6 T7 R : Type}
(f: T1 → T2 → T3 → T4 → T5 → T6 → T7 → R)
(arg1 : T1)
(arg2 : T2)
(arg3 : T3)
(arg4 : T4)
(arg5 : T5)
(arg6 : T6)
(arg7 : T7)
:
{r : R & r = f arg1 arg2 arg3 arg4 arg5 arg6 arg7}
.
Program Definition expand_total
{ar ea sa : nat}
(construct : @MLConstruct ar ea sa Σ)
(args : vec PMPattern ar)
(bevars : vec EVarName ea)
(bsvars : vec SVarName sa)
(f : ∀ (p : PMPattern), p ∈ (vec_to_list args) → Pattern_in_context)
: Pattern_in_context :=
match (eq_apply_4 (mlc_expand ar ea sa) construct (list_map_pfin (vec_to_list args) (fun p ⇒ fun pf ⇒ f p pf)) bevars bsvars) with
| existT None Hcontra ⇒ @False_rec _ _
| existT (Some phi) _ ⇒ phi
end.
Equations? PMPattern_to_ln
(ϕ : PMPattern)
: Pattern_in_context by wf (PMPattern_size ϕ) lt := {
PMPattern_to_ln (pmpatt_inj ln _) := mkPIC _ (fun _ ⇒ ln ) _;
PMPattern_to_ln (pmpatt_construct construct args bevars bsvars) :=
expand_total construct args bevars bsvars (fun p pf ⇒ PMPattern_to_ln p)
}
.
Program Definition mlc_sym
(s : symbols)
: MLConstruct 0 0 0 := {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some (
mkPIC _ (
fun _ ⇒
patt_sym s
) (
fun _ ⇒ _
)
)
|}
.
Program Definition mlc_bott
: MLConstruct 0 0 0 := {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some(
mkPIC _ (
fun _ ⇒
patt_bott
) (
fun _ ⇒ _
)
)
|}
.
Program Definition mlc_evar
(name : EVarName)
: MLConstruct 0 0 0 := {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some (mkPIC _ (
fun ctx ⇒
match (pc_evm ctx) !! name with
| Some n ⇒ patt_bound_evar n
| None ⇒ patt_free_evar (string2evar name)
end
) _ )
|}
.
Lemma wfp_update_evm_key ϕic new_name old_name pc:
well_formed_positive (pic_pic ϕic pc) = true →
well_formed_positive (pic_pic ϕic (update_evm_key new_name old_name pc)) = true.
Lemma wfp_update_svm_key ϕic new_name old_name pc:
well_formed_positive (pic_pic ϕic pc) = true →
well_formed_positive (pic_pic ϕic (update_svm_key new_name old_name pc)) = true.
Lemma boundary_value_update_key new_name old_name store:
boundary_value (update_key new_name old_name store)
= boundary_value store
.
Lemma wfcex_update_evm_key ϕic new_name old_name pc:
well_formed_closed_ex_aux (pic_pic ϕic pc) (boundary_value (pc_evm pc)) = true →
well_formed_closed_ex_aux
(pic_pic ϕic (update_evm_key new_name old_name pc))
(boundary_value (pc_evm pc)) = true
.
Lemma wfcmu_update_svm_key ϕic new_name old_name pc:
well_formed_closed_mu_aux (pic_pic ϕic pc) (boundary_value (pc_svm pc)) = true →
well_formed_closed_mu_aux
(pic_pic ϕic (update_svm_key new_name old_name pc))
(boundary_value (pc_svm pc)) = true
.
Program Definition mlc_evar_rename
(new_name old_name : EVarName)
: MLConstruct 1 0 0 := {|
mlc_expand :=
fun ps _ _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let new_ctx := update_evm_key new_name old_name ctx in
pic_pic ϕ_in_context new_ctx
) _ )
end
|}
.
Program Definition mlc_svar_rename
(new_name old_name : SVarName)
: MLConstruct 1 0 0 := {|
mlc_expand :=
fun ps _ _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let new_ctx := update_svm_key new_name old_name ctx in
pic_pic ϕ_in_context new_ctx
) _ )
end
|}
.
Program Definition mlc_svar
(name : SVarName)
: MLConstruct 0 0 0:= {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some (mkPIC _ (
fun ctx ⇒
match (pc_svm ctx) !! name with
| Some n ⇒ patt_bound_svar n
| None ⇒ patt_free_svar (string2svar name)
end
) _ )
|}
.
Program Definition mlc_app
: MLConstruct 2 0 0 := {|
mlc_expand :=
fun ps ⇒
fun _ ⇒
fun _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ₁ ⇒
match ps !! 1 with
| None ⇒ None
| Some ϕ₂ ⇒
Some (mkPIC _ (
fun ctx ⇒
patt_app (pic_pic ϕ₁ ctx) (pic_pic ϕ₂ ctx)
) _
)
end
end
|}
.
Program Definition mlc_imp
: MLConstruct 2 0 0 := {|
mlc_expand :=
fun ps ⇒
fun _ ⇒
fun _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ₁ ⇒
match ps !! 1 with
| None ⇒ None
| Some ϕ₂ ⇒
Some ( mkPIC _ (
fun ctx ⇒
patt_imp (pic_pic ϕ₁ ctx) (pic_pic ϕ₂ ctx)
) _ )
end
end
|}
.
Lemma S_max_list (l : list nat) :
S (max_list l) = match l with [] ⇒ 1 | _ ⇒ max_list (S <$> l) end
.
Lemma map_fold_fmap
(X : Type)
(g: VarName → nat → X → X)
(gcom: ∀ j1 z1 j2 z2 y, g j1 z1 (g j2 z2 y) = g j2 z2 (g j1 z1 y))
(f : nat → nat)
(m : gmap VarName nat)
(x : X)
: map_fold g x (f <$> m) = map_fold (fun vn n x ⇒ g vn (f n) x) x m
.
Instance pred_S_cancel : Cancel (=) Nat.pred S.
Lemma map_fold_compose
(X : Type)
(g: VarName → nat → X → X)
(f finv : X → X)
{f_finv_cancel : Cancel (=) finv f}
(gcom: ∀ j1 z1 j2 z2 y, g j1 z1 (g j2 z2 y) = g j2 z2 (g j1 z1 y))
(fgcom: ∀ j1 z1 j2 z2 y, f (g j1 z1 ((g j2 z2 y))) = f (g j2 z2 ((g j1 z1 y))))
(m : gmap VarName nat)
(x : X)
: f (map_fold g x m) = map_fold (fun vn n x ⇒ f (g vn n (finv x))) (f x) m
.
Lemma max_helper_lemma v m:
v `max` map_fold (λ (_ : VarName) (v0 r : nat), v0 `max` r) 0 m =
v `max` map_fold (λ (_ : VarName) (v0 r : nat), v0 `max` r) v m.
Lemma max_value_in_param
(m : gmap VarName nat)
(name : VarName)
(v : nat)
:
m !! name = Some v →
max_value 0 m = max_value v m
.
Lemma boundary_value_incr_values m name:
m !! name = None →
boundary_value (<[name:=0]>(incr_values m))
= S (boundary_value m)
.
Program Definition mlc_exists
: MLConstruct 1 1 0 := {|
mlc_expand :=
fun ps ⇒
fun evs ⇒
fun _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
match evs !! 0 with
| None ⇒ None
| Some name ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let name' := this_or_fresh name (pc_evm ctx) in
let ctx' := pc_add_ename ctx name' in
let ϕ := pic_pic ϕ_in_context ctx' in
patt_exists ϕ
) _ )
end
end
|}
.
Program Definition mlc_mu
: MLConstruct 1 0 1 := {|
mlc_expand :=
fun ps ⇒
fun _ ⇒
fun svs ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
match svs !! 0 with
| None ⇒ None
| Some name ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let name' := this_or_fresh name (pc_svm ctx) in
let ctx' := pc_add_sname ctx name' in
let ϕ := pic_pic ϕ_in_context ctx' in
patt_mu ϕ
) _ )
end
end
|}
.
Section examples.
Context
{s1 : symbols}
.
Local Example ex_1 : PMPattern :=
pmpatt_construct (mlc_sym s1) vnil vnil vnil
.
Local Example Ex_2 : PMPattern :=
pmpatt_construct (mlc_imp)
[# ex_1; ex_1] vnil vnil.
End examples.
End sec.
From MatchingLogic Require Export
Signature
Pattern
.
From stdpp Require Export
strings
stringmap
.
Require Import String.
Equations? list_map_pfin
{A B : Type}
(l : list A)
(f : ∀ (x : A) (pf: x ∈ l), B)
: list B :=
list_map_pfin [] _ := [] ;
list_map_pfin (x::xs) f := (f x _)::(list_map_pfin xs (fun x H ⇒ f x _)) .
Lemma list_map_pfin_spec {A B : Type} (f : A → B) (l : list A) :
list_map_pfin l (fun (x : A) (_ : x ∈ l) ⇒ f x) = List.map f l.
Lemma length_list_map_pfin
{A B : Type}
(l : list A)
(f : ∀ (x : A) (pf: x ∈ l), B)
:
List.length (list_map_pfin l f) = List.length l
.
Definition VarName := string.
Definition EVarName := VarName.
Definition SVarName := VarName.
Definition incr_values
(vm : gmap VarName nat)
: gmap VarName nat
:= fmap (fun n ⇒ S n) vm.
(*
Represents a context in which a pattern is well-defined.
In particular, `pc_evm` is the set of element variables in context.
*)
Record PContext := mkPContext {
pc_evm : gmap EVarName nat ;
pc_svm : gmap SVarName nat ;
}.
(*Compute (fresh_string "X" (<"X" := 1>∅)).*)
Definition this_or_fresh
(this : VarName)
(g : gmap VarName nat)
: VarName
:=
fresh_string this g
.
Lemma this_or_fresh_fresh this g:
g !! (this_or_fresh this g) = None.
Definition renaming_function
(new_key old_key some_key : VarName) : VarName :=
match (decide (some_key = old_key)) with
| left _ ⇒ new_key
| right _ ⇒
match (decide (some_key = new_key)) with
| left _ ⇒ old_key
| right _ ⇒ some_key
end
end.
#[global]
Instance renaming_function_injective new_name old_name:
Inj eq eq (renaming_function new_name old_name).
Definition update_key
(new_key old_key : VarName)
(m : gmap VarName nat)
: gmap VarName nat
:= kmap (renaming_function new_key old_key) m
.
Definition update_evm_key
(new_key old_key : EVarName)
(pctx : PContext)
: PContext
:= mkPContext
(update_key new_key old_key (pc_evm pctx))
(pc_svm pctx)
.
Definition update_svm_key
(new_key old_key : SVarName)
(pctx : PContext)
: PContext
:= mkPContext
(pc_evm pctx)
(update_key new_key old_key (pc_svm pctx))
.
Definition max_value (d : nat) (m : gmap VarName nat) : nat :=
map_fold (fun k v r ⇒ Nat.max v r) d m
.
Lemma max_value_kmap (f : VarName → VarName) {injF : Inj eq eq f} (d : nat) (m : gmap VarName nat):
max_value d (kmap f m) = max_value d m
.
Lemma max_value_in_leq
(m : gmap VarName nat)
(d : nat)
(name : VarName)
:
m !! name = Some d →
d ≤ max_value 0 m
.
Definition boundary_value (m : gmap VarName nat) : nat :=
match (decide (m = ∅)) with
| left _ ⇒ 0
| right _ ⇒ S (max_value 0 m)
end
.
Definition pc_add_ename
(ctx : PContext)
(name : EVarName) :=
mkPContext ((<[name := 0]>(incr_values (pc_evm ctx)))) (pc_svm ctx)
.
Definition pc_add_sname
(ctx : PContext)
(name : SVarName) :=
mkPContext (pc_evm ctx) ((<[name := 0]>(incr_values (pc_svm ctx))))
.
Record Pattern_in_context
{Σ : Signature} := mkPIC {
pic_pic: PContext → Pattern;
pic_wf : ∀ (pc : PContext),
let phi := pic_pic pc in
well_formed_positive phi ∧ (* TODO no_negative, no_positive_occurrence*)
well_formed_closed_ex_aux phi (boundary_value (pc_evm pc)) ∧
well_formed_closed_mu_aux phi (boundary_value (pc_svm pc)) ;
}
.
(*
So what notations we want to support?
¬ϕ ≡ ϕ ---> ⊥
ϕ₁ \/ ϕ₂ ≡ ¬ϕ₁ ---> ϕ₂
∀ x. ϕ ≡ ¬ ∃ x. ¬ ϕ
So, a notation is parametric in
(1) how many patterns it takes as an argument.
(2) how many element variables it binds
(3) how many set variables it binds.
*)
Record MLConstruct
(mlc_arity : nat)
(mlc_ebinder_arity : nat)
(mlc_sbinder_arity : nat)
{Σ : Signature} := {
(*mlc_level : nat ;*)
mlc_expand :
list Pattern_in_context → (* patterns *)
list EVarName → (* bound evars*)
list SVarName → (* bound svars*)
option Pattern_in_context ;
mlc_expand_almost_total :
∀
(args : list Pattern_in_context)
(ebinders : list EVarName)
(sbinders : list SVarName),
List.length args = mlc_arity →
List.length ebinders = mlc_ebinder_arity →
List.length sbinders = mlc_sbinder_arity →
∃ ϕ_in_context,
mlc_expand args ebinders sbinders = Some ϕ_in_context ;
}.
Section sec.
Context
{Σ : Signature}
.
Inductive PMPattern : Set :=
| pmpatt_inj (ln : Pattern) (wfpf : Pattern.well_formed ln)
| pmpatt_construct
{a ea sa : nat}
(construct : MLConstruct a ea sa)
(args : vec PMPattern a)
(bound_evars : vec EVarName ea)
(bound_svars : vec SVarName sa)
.
Equations PMPattern_size
(ϕ : PMPattern)
: nat := {
PMPattern_size (pmpatt_inj _ _) := 1 ;
PMPattern_size (pmpatt_construct _ args _ _) :=
S (@PMPattern_size_vec _ args)
where PMPattern_size_vec
{arity : nat}
(v : vec PMPattern arity)
: nat := {
@PMPattern_size_vec _ vnil := 1 ;
@PMPattern_size_vec _ (vcons x xs) :=
(PMPattern_size x + PMPattern_size_vec xs)
}
}
.
Lemma PMPattern_size_clause_2_PMPattern_size_vec_spec
(ar1 ea1 sa1 : nat) (con : MLConstruct ar1 ea1 sa1) a e s ar args':
@PMPattern_size_clause_2_PMPattern_size_vec PMPattern_size ar1 ea1 sa1 con a e s ar args'
= S (list_sum (fmap (fun p ⇒ PMPattern_size p) (vec_to_list args')))
.
Equations eq_apply_4
{T1 T2 T3 T4 R : Type}
(f: T1 → T2 → T3 → T4 → R)
(arg1 : T1)
(arg2 : T2)
(arg3 : T3)
(arg4 : T4)
:
{r : R & r = f arg1 arg2 arg3 arg4} :=
eq_apply_4 f arg1 arg2 arg3 arg4
:= existT (f arg1 arg2 arg3 arg4) (@eq_refl _ _) .
Definition eq_apply_5
{T1 T2 T3 T4 T5 R : Type}
(f: T1 → T2 → T3 → T4 → T5 → R)
(arg1 : T1)
(arg2 : T2)
(arg3 : T3)
(arg4 : T4)
(arg5 : T5)
:
{r : R & r = f arg1 arg2 arg3 arg4 arg5}
.
Definition eq_apply_7
{T1 T2 T3 T4 T5 T6 T7 R : Type}
(f: T1 → T2 → T3 → T4 → T5 → T6 → T7 → R)
(arg1 : T1)
(arg2 : T2)
(arg3 : T3)
(arg4 : T4)
(arg5 : T5)
(arg6 : T6)
(arg7 : T7)
:
{r : R & r = f arg1 arg2 arg3 arg4 arg5 arg6 arg7}
.
Program Definition expand_total
{ar ea sa : nat}
(construct : @MLConstruct ar ea sa Σ)
(args : vec PMPattern ar)
(bevars : vec EVarName ea)
(bsvars : vec SVarName sa)
(f : ∀ (p : PMPattern), p ∈ (vec_to_list args) → Pattern_in_context)
: Pattern_in_context :=
match (eq_apply_4 (mlc_expand ar ea sa) construct (list_map_pfin (vec_to_list args) (fun p ⇒ fun pf ⇒ f p pf)) bevars bsvars) with
| existT None Hcontra ⇒ @False_rec _ _
| existT (Some phi) _ ⇒ phi
end.
Equations? PMPattern_to_ln
(ϕ : PMPattern)
: Pattern_in_context by wf (PMPattern_size ϕ) lt := {
PMPattern_to_ln (pmpatt_inj ln _) := mkPIC _ (fun _ ⇒ ln ) _;
PMPattern_to_ln (pmpatt_construct construct args bevars bsvars) :=
expand_total construct args bevars bsvars (fun p pf ⇒ PMPattern_to_ln p)
}
.
Program Definition mlc_sym
(s : symbols)
: MLConstruct 0 0 0 := {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some (
mkPIC _ (
fun _ ⇒
patt_sym s
) (
fun _ ⇒ _
)
)
|}
.
Program Definition mlc_bott
: MLConstruct 0 0 0 := {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some(
mkPIC _ (
fun _ ⇒
patt_bott
) (
fun _ ⇒ _
)
)
|}
.
Program Definition mlc_evar
(name : EVarName)
: MLConstruct 0 0 0 := {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some (mkPIC _ (
fun ctx ⇒
match (pc_evm ctx) !! name with
| Some n ⇒ patt_bound_evar n
| None ⇒ patt_free_evar (string2evar name)
end
) _ )
|}
.
Lemma wfp_update_evm_key ϕic new_name old_name pc:
well_formed_positive (pic_pic ϕic pc) = true →
well_formed_positive (pic_pic ϕic (update_evm_key new_name old_name pc)) = true.
Lemma wfp_update_svm_key ϕic new_name old_name pc:
well_formed_positive (pic_pic ϕic pc) = true →
well_formed_positive (pic_pic ϕic (update_svm_key new_name old_name pc)) = true.
Lemma boundary_value_update_key new_name old_name store:
boundary_value (update_key new_name old_name store)
= boundary_value store
.
Lemma wfcex_update_evm_key ϕic new_name old_name pc:
well_formed_closed_ex_aux (pic_pic ϕic pc) (boundary_value (pc_evm pc)) = true →
well_formed_closed_ex_aux
(pic_pic ϕic (update_evm_key new_name old_name pc))
(boundary_value (pc_evm pc)) = true
.
Lemma wfcmu_update_svm_key ϕic new_name old_name pc:
well_formed_closed_mu_aux (pic_pic ϕic pc) (boundary_value (pc_svm pc)) = true →
well_formed_closed_mu_aux
(pic_pic ϕic (update_svm_key new_name old_name pc))
(boundary_value (pc_svm pc)) = true
.
Program Definition mlc_evar_rename
(new_name old_name : EVarName)
: MLConstruct 1 0 0 := {|
mlc_expand :=
fun ps _ _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let new_ctx := update_evm_key new_name old_name ctx in
pic_pic ϕ_in_context new_ctx
) _ )
end
|}
.
Program Definition mlc_svar_rename
(new_name old_name : SVarName)
: MLConstruct 1 0 0 := {|
mlc_expand :=
fun ps _ _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let new_ctx := update_svm_key new_name old_name ctx in
pic_pic ϕ_in_context new_ctx
) _ )
end
|}
.
Program Definition mlc_svar
(name : SVarName)
: MLConstruct 0 0 0:= {|
mlc_expand :=
fun _ ⇒
fun _ ⇒
fun _ ⇒ Some (mkPIC _ (
fun ctx ⇒
match (pc_svm ctx) !! name with
| Some n ⇒ patt_bound_svar n
| None ⇒ patt_free_svar (string2svar name)
end
) _ )
|}
.
Program Definition mlc_app
: MLConstruct 2 0 0 := {|
mlc_expand :=
fun ps ⇒
fun _ ⇒
fun _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ₁ ⇒
match ps !! 1 with
| None ⇒ None
| Some ϕ₂ ⇒
Some (mkPIC _ (
fun ctx ⇒
patt_app (pic_pic ϕ₁ ctx) (pic_pic ϕ₂ ctx)
) _
)
end
end
|}
.
Program Definition mlc_imp
: MLConstruct 2 0 0 := {|
mlc_expand :=
fun ps ⇒
fun _ ⇒
fun _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ₁ ⇒
match ps !! 1 with
| None ⇒ None
| Some ϕ₂ ⇒
Some ( mkPIC _ (
fun ctx ⇒
patt_imp (pic_pic ϕ₁ ctx) (pic_pic ϕ₂ ctx)
) _ )
end
end
|}
.
Lemma S_max_list (l : list nat) :
S (max_list l) = match l with [] ⇒ 1 | _ ⇒ max_list (S <$> l) end
.
Lemma map_fold_fmap
(X : Type)
(g: VarName → nat → X → X)
(gcom: ∀ j1 z1 j2 z2 y, g j1 z1 (g j2 z2 y) = g j2 z2 (g j1 z1 y))
(f : nat → nat)
(m : gmap VarName nat)
(x : X)
: map_fold g x (f <$> m) = map_fold (fun vn n x ⇒ g vn (f n) x) x m
.
Instance pred_S_cancel : Cancel (=) Nat.pred S.
Lemma map_fold_compose
(X : Type)
(g: VarName → nat → X → X)
(f finv : X → X)
{f_finv_cancel : Cancel (=) finv f}
(gcom: ∀ j1 z1 j2 z2 y, g j1 z1 (g j2 z2 y) = g j2 z2 (g j1 z1 y))
(fgcom: ∀ j1 z1 j2 z2 y, f (g j1 z1 ((g j2 z2 y))) = f (g j2 z2 ((g j1 z1 y))))
(m : gmap VarName nat)
(x : X)
: f (map_fold g x m) = map_fold (fun vn n x ⇒ f (g vn n (finv x))) (f x) m
.
Lemma max_helper_lemma v m:
v `max` map_fold (λ (_ : VarName) (v0 r : nat), v0 `max` r) 0 m =
v `max` map_fold (λ (_ : VarName) (v0 r : nat), v0 `max` r) v m.
Lemma max_value_in_param
(m : gmap VarName nat)
(name : VarName)
(v : nat)
:
m !! name = Some v →
max_value 0 m = max_value v m
.
Lemma boundary_value_incr_values m name:
m !! name = None →
boundary_value (<[name:=0]>(incr_values m))
= S (boundary_value m)
.
Program Definition mlc_exists
: MLConstruct 1 1 0 := {|
mlc_expand :=
fun ps ⇒
fun evs ⇒
fun _ ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
match evs !! 0 with
| None ⇒ None
| Some name ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let name' := this_or_fresh name (pc_evm ctx) in
let ctx' := pc_add_ename ctx name' in
let ϕ := pic_pic ϕ_in_context ctx' in
patt_exists ϕ
) _ )
end
end
|}
.
Program Definition mlc_mu
: MLConstruct 1 0 1 := {|
mlc_expand :=
fun ps ⇒
fun _ ⇒
fun svs ⇒
match ps !! 0 with
| None ⇒ None
| Some ϕ_in_context ⇒
match svs !! 0 with
| None ⇒ None
| Some name ⇒
Some ( mkPIC _ (
fun ctx : PContext ⇒
let name' := this_or_fresh name (pc_svm ctx) in
let ctx' := pc_add_sname ctx name' in
let ϕ := pic_pic ϕ_in_context ctx' in
patt_mu ϕ
) _ )
end
end
|}
.
Section examples.
Context
{s1 : symbols}
.
Local Example ex_1 : PMPattern :=
pmpatt_construct (mlc_sym s1) vnil vnil vnil
.
Local Example Ex_2 : PMPattern :=
pmpatt_construct (mlc_imp)
[# ex_1; ex_1] vnil vnil.
End examples.
End sec.
This page has been generated by coqdoc