Library CFGV

Require Export GVariables.
Set Implicit Arguments.

used in bindingInfoCorrect below. Also, see ValidIndicesDecidable below
Definition ValidIndices {A B : Type}
(bindingInfo : list (nat × nat))
(rhsSyms : list (A + B)) : [univ]
:= (
n m,
LIn (n,m) bindingInfo
→ (m < length rhsSyms) × (n < length rhsSyms)
× (true = liftNth isInl rhsSyms n)
)
×
(
n,
(true = liftNth isInl rhsSyms n)
→ LIn n (map (@fst _ _) bindingInfo)
)
×no_repeats bindingInfo.

For concretely specified grammars, one can just compute the following lemma to get the proof of ValidIndices. See the tactic (Ltac) proveBindingInfoCorrect below.
Lemma ValidIndicesDecidable:
{A B : Type}
(bindingInfo : list (nat × nat))
(rhsSyms : list (A + B)),
decidable (ValidIndices bindingInfo rhsSyms).
Proof.
intros.
unfold ValidIndices.
apply decidable_prod;[|apply decidable_prod].
- induction bindingInfo as [| (n,m) bindingInfo Hind];
[left; dands |]; cpx.
dorn Hind;[| right]; cpx.
remember (liftNth isInl rhsSyms n) as bl.
destruct (lt_dec m (length rhsSyms));
destruct (lt_dec n (length rhsSyms));
destruct bl; try rewrite <- Heqbl;
try(left; introv Hin; repeat(in_reasoning); cpx; fail);
[| | | | | | ];
right; introv Hin;
specialize (Hin _ _ (inl eq_refl));
try rewrite <- Heqbl in Hin;
dands; cpx.

- remember ((map (fst (B:=nat)) bindingInfo)) as bif.
clear dependent bindingInfo.
revert bif. unfold liftNth;
induction rhsSyms as [| rs rhsSyms Hind];
[left; intro n; destruct n;
simpl; cpx |].
intro bifCons.
remember (flat_map
(fun nmatch n with
|0 ⇒ []
| S m[m] end) bifCons)
as bif.
specialize (Hind bif).
dorn Hind; [| right]; cpx.
+ destruct rs as [sa| sb];[|left; destruct n;
allsimpl; cpx].
× destruct (in_deq _ deq_nat 0 bifCons); cpx;
[left; destruct n | right]; simpl;
subst bif; cpx;[].

introv Heq.
apply Hind in Heq.
apply lin_flat_map in Heq.
exrepnd.
destruct x; cpx.
inverts Heq0; cpx; fail.

× introv Heq. subst bif.
specialize (Hind ( n)).
apply Hind in Heq. clear Hind.
apply lin_flat_map in Heq.
exrepnd. destruct x; cpx.
inverts Heq0; cpx.
+ introv Hc. apply Hind. clear Hind. introv Heq.
subst bif. apply lin_flat_map.
specialize (Hc (S n)). simpl in Hc.
apply Hc in Heq.
(S n). dands; cpx.

- apply no_repeat_dec. apply deq_prod; exact deq_nat.
Defined.

CatchFileBetweenTagsCFGVStart
Record CFGV := {
Terminal : Type; VarSym : Type;
TNonTerminal : Type; PNonTerminal : Type;

PatProd : Type; EmbedProd : Type; TermProd : Type;

varSem : VarSymVarType;
vSubstType : VarSymTNonTerminal;
tSemType : TerminalType;

ppLhsRhs: PatProd
(PNonTerminal × list (PNonTerminal
+ (Terminal + VarSym)));

epLhsRhs : EmbedProd → (PNonTerminal × TNonTerminal);

tpLhsRhs: TermProd
(TNonTerminal × list ((PNonTerminal + VarSym)
+(Terminal+TNonTerminal)));

bindingInfo : TermProdlist (nat × nat);
bindingInfoCorrect: (p: TermProd),
ValidIndices (bindingInfo p) (snd (tpLhsRhs p));
}. CatchFileBetweenTagsCFGVEnd

DeqVarSym : Deq VarSym;
deqT : Deq Terminal;
deqNT : Deq TNonTerminal;
deqPT : Deq PNonTerminal;
deqPr : Deq TermProd;
deqEm : Deq EmbedProd;
deqPPr : Deq PatProd;
deqTSem : (t: Terminal), Deq (tSemType t)

}.

Definition vType {G: CFGV} (vc : VarSym G) : Type :=
(typ (varSem G vc)).

A more intuitive way to denote symbols of a CFGV : instead of inl inr....
CatchFileBetweenTagsGSymStart
Inductive GSym (G: CFGV) : Type :=
| gsymT : Terminal GGSym G
| gsymV : VarSym GGSym G
| gsymTN : TNonTerminal GGSym G
| gsymPN : PNonTerminal GGSym G.
CatchFileBetweenTagsGSymEnd
Make the CFGV argument implicit
Arguments gsymT {G} _.
Arguments gsymV {G} _.
Arguments gsymTN {G} _.
Arguments gsymPN {G} _.

Arguments bindingInfo {c} _.

Lemma deqGSym : (G: CFGV),
Deq (GSym G).
Proof.
intros.
intros sa sb.
destruct sa as [sa|sa|sa|sa]; destruct sb as [sb|sb|sb|sb];
try (right; introv Hc; inverts Hc; cpx; fail).
- destruct (deqT G sa sb);[left; subst|right; introv HC; inverts HC]; cpx.
- destruct (DeqVarSym G sa sb);[left; subst|right; introv HC; inverts HC]; cpx.
- destruct (deqNT G sa sb);[left; subst|right; introv HC; inverts HC]; cpx.
- destruct (deqPT G sa sb);[left; subst|right; introv HC; inverts HC]; cpx.
Defined.

Hint Resolve deqT deqTSem DeqVarSym deqNT deqPT deqGSym deqPr deqEm deqPPr: Deq.

Definition prhs_aux {G : CFGV}
(symSum :((PNonTerminal G + VarSym G)
+(Terminal G + TNonTerminal G))) : (GSym G) :=
match symSum with
| inl (inl p) ⇒ gsymPN p
| inl (inr vc) ⇒ gsymV vc
| inr (inl t) ⇒ gsymT t
| inr (inr nt) ⇒ gsymTN nt
end.

Definition tpRhsSym {G: CFGV} (p:TermProd G) : list (GSym G)
:=map (prhs_aux) (snd (tpLhsRhs G p)).

Definition ptrhs_aux {G : CFGV}
(symSum :((PNonTerminal G)+ (Terminal G + VarSym G)))
: (GSym G) :=
match symSum with
| (inl p) ⇒ gsymPN p
| inr (inl t) ⇒ gsymT t
| inr (inr v) ⇒ gsymV v
end.

Definition gsymNotNT {G : CFGV} (s : GSym G) :=
match s with
| gsymT _True
| gsymV _True
| gsymTN _False
| gsymPN _True
end.

Lemma ptrhs_aux_nonNT : {G: CFGV}
(symSum :((PNonTerminal G)+ (Terminal G + VarSym G))) ,
gsymNotNT (ptrhs_aux symSum).
Proof.
intros.
dorn symSum;[|dorn symSum]; simpl; auto.
Qed.

Definition ppRhsSym {G: CFGV} (p:PatProd G) : list (GSym G)
:=map (ptrhs_aux) (snd (ppLhsRhs G p)).

Definition tpLhs (G: CFGV) (p:TermProd G) : TNonTerminal G
:= (fst (tpLhsRhs G p)).

Definition epLhs (G: CFGV) (p:EmbedProd G) : PNonTerminal G
:= (fst (epLhsRhs G p)).

Definition epRhs (G: CFGV) (p:EmbedProd G) : TNonTerminal G
:= (snd (epLhsRhs G p)).

Definition ppLhs (G: CFGV) (p:PatProd G) : PNonTerminal G
:= (fst (ppLhsRhs G p)).

Definition gsymNotP {G : CFGV} (s : GSym G) :=
match s with
| gsymT _True
| gsymV _True
| gsymTN _True
| gsymPN _False
end.

Arguments DeqVarSym {c} _ _.

Definition flatten {A : Type} (l : list (list A)) : list A:=
flat_map (fun xx) l.

Definition bindCount {G : CFGV} (p: TermProd G) (n : nat) :=
let lnat := (map (@fst _ _) (bindingInfo p))
in count_occ deq_nat lnat n.

Definition prhsIsBound {G : CFGV} (p: TermProd G) : list bool :=
(map isInl (snd (tpLhsRhs G p))).

Definition MixtureParam {G : CFGV} :=
list (bool × (GSym G)).

Definition MParamCorrectb {G : CFGV} (pp: @MixtureParam G)
: bool :=
forallb (fun pmatch p with
| (false, gsymPN _)false
| _true
end)
pp.

Definition tpRhsAugIsPat {G : CFGV} (p: TermProd G)
: MixtureParam :=
combine (prhsIsBound p) (tpRhsSym p).

Definition bindingSourcesNth {G:CFGV}
(p: TermProd G) (k:nat) : list nat :=
flat_map
(fun pp : (nat × nat)
⇒ let (n,m) := pp in
if (beq_nat k m) then [n] else [])
(bindingInfo p).

Definition ValidNthSrc (len : nat) (ln: list nat):=
no_repeats ln
× lForall (fun nn < len) ln.

Lemma bsNthValid : {G:CFGV}
(p: TermProd G) (k:nat),
ValidNthSrc (length (tpRhsSym p)) (bindingSourcesNth p k).
Proof.
intros. unfold ValidNthSrc.
unfold bindingSourcesNth, bindingInfo, tpRhsSym.
autorewrite with fast.
pose proof (bindingInfoCorrect G p) as XX.
destruct (tpLhsRhs G p) as [lhs ls].
destruct G; allsimpl; cpx.

allsimpl. remember ((bindingInfo0 p)) as bi. clear Heqbi.
allsimpl. clear bindingInfoCorrect0.
repnud XX. clear XX1.
induction bi; dands; allsimpl; cpx;
allrw no_repeats_cons;
exrepnd;

apply IHbi in XX1; exrepnd; cpx;
remember (beq_nat k a) as bn; destruct bn; cpx;
allrw no_repeats_cons; allsimpl; dands; cpx.
- introv Hin. rw lin_flat_map in Hin.
exrepnd.
remember (beq_nat k x) as bkx; destruct bkx; allsimpl; cpx.
dorn Hin0; subst; cpx.
allapply beq_nat_eq.
subst. subst. cpx.
- pose proof (XX0 _ _ (inl eq_refl)).
repnd; cpx.
Qed.

Definition bndngPatIndices {G:CFGV}
(p: TermProd G) : list (list nat) :=
map (bindingSourcesNth p) (seq 0 (length (tpRhsSym p))).

Definition validBsl (len:nat) (lln: list (list nat)) :=
lforall (ValidNthSrc len) lln.

Lemma bndngPatIndicesValid :
{G:CFGV} (p: TermProd G),
validBsl (length (tpRhsSym p)) (bndngPatIndices p).
Proof.
intros.
unfolds_base.
unfold bndngPatIndices.
introv Hin.
apply in_map_iff in Hin.
exrepnd.
subst.
apply bsNthValid.
Qed.

Lemma bndngPatIndicesValid2 :
{G:CFGV} (p: TermProd G),
validBsl (length (snd (tpLhsRhs G p))) (bndngPatIndices p).
Proof.
intros.
pose proof (bndngPatIndicesValid p) as X.
unfold tpRhsSym in X.
autorewrite with fast in X.
trivial.
Qed.

Lemma DeqVtype : {G:CFGV} (vc : VarSym G),
Deq (vType vc).
Proof.
intros. unfold vType.
match goal with
[ |- Deq (typ ?xx)] ⇒ destruct xx as [? vd]
end.
repnud vd. auto.
Defined.

Hint Resolve DeqVtype : Deq.

Definition vFreshVar
{G : CFGV}
{vc : VarSym G}
(lvAvoid: list (vType vc))
(v: (vType vc)) : vType vc :=
((fresh (varSem G vc)) lvAvoid [v]).

Definition GFreshVars
{G : CFGV}
{vc : VarSym G}
(lvAvoid: list (vType vc))
(lv: list (vType vc)) : list (vType vc) :=
(FreshDistinctVars (varSem G vc) lv lvAvoid).

{G : CFGV} {vc : VarSym G}
(lvAvoid: list (vType vc))
(lv: list (vType vc)),
let lvn := (GFreshVars lvAvoid lv) in
no_repeats lvn × disjoint lvn lvAvoid × length lvn= length lv.
Proof.
intros.
subst lvn.
unfold GFreshVars.
pose proof(
allsimpl.
exrepnd; dands; cpx.
Qed.

Lemma vFreshVarSpec :
{G : CFGV}
{vc : VarSym G}
(lvAvoid: list (vType vc))
(v: (vType vc)),
! LIn (vFreshVar lvAvoid v) lvAvoid.
Proof.
intros.
unfold vFreshVar.
revert v. revert lvAvoid.
unfold vType.
destruct (varSem G vc) as [T vd Vf Vfc].
allsimpl.
exrepnd. allsimpl.
cpx.
Qed.

also guaranteed to be different from the input
Definition vFreshDiff
{G : CFGV}
{vc : VarSym G}
(lvAvoid: list (vType vc))
(v: (vType vc)) :=
(fresh (varSem G vc)) (v::lvAvoid) [v].

Lemma vFreshDiffSpec :
{G : CFGV}
{vc : VarSym G}
(lvAvoid: list (vType vc))
(v: (vType vc)),
! LIn (vFreshDiff (lvAvoid) v) (v::lvAvoid).
Proof.
intros.
apply vFreshVarSpec.
Qed.

Lemma length_pRhsAugIsPat : {G : CFGV} (p : TermProd G),
length (tpRhsAugIsPat p) = length ((snd (tpLhsRhs G p))).
Proof.
intros. simpl.
unfold tpRhsAugIsPat, prhsIsBound , tpRhsSym.
rewrite combine_length.
autorewrite with fast.
rewrite min_eq; refl.
Qed.

Lemma GFreshDistRenWSpec:
{G:CFGV} (vc : VarSym G)
(lv :list (vType vc))
(lvAvoid :list (vType vc)),
{lvn : list (vType vc) \$
no_repeats lvn × disjoint lvn lvAvoid
× length lvn= length lv}.
Proof.
intros. eapply FreshDistRenWSpec; eauto.
Defined.

Lemma deqMixP : {G}, Deq (@MixtureParam G).
Proof.
unfold MixtureParam.
eauto with Deq.
Defined.

Lemma deqSigVType :
{G}, (Deq (sigT (@vType G))).
Proof.
intros.
apply sigTDeq;
eauto with Deq.
Defined.

Lemma deqSigTSemType :
{G}, (Deq (sigT (tSemType G))).
Proof.
intros.
apply sigTDeq;
eauto with Deq.
Defined.

Definition decDisjointV {G} (vc : VarSym G)
(la lb : list (vType vc)) :
(disjoint la lb[+]!disjoint la lb)
:= dec_disjoint (DeqVtype vc) la lb.

Ltac proveBindingInfoCorrect :=
let p:= fresh "tprod" in
let d:= fresh "decVal" in
let Heqd:= fresh "Heq" d in
intro p;
match goal with
[ |- ValidIndices ?binf ?rhsSyms ] ⇒
remember (ValidIndicesDecidable binf rhsSyms) as d eqn:Heqd;
destruct p; unfold ValidIndicesDecidable in Heqd; allsimpl;
destruct d; auto; inverts Heqd
end.

Ltac proveDeqInductiveNonrec :=
let x:= fresh "xdl" in
let y:= fresh "axr" in
let Hc:= fresh "Hcontra" in
intros x y ; destruct x; destruct y;
try (left; cpx; fail); (try right; introv Hc; inverts Hc ; cpx).