From Undecidability.L Require Import Eval.
From Undecidability.FOLC Require Import Extend FOL Syntax.
From Undecidability.L Require Import Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode Datatypes.Lists Reductions.H10_to_L Datatypes.LNat Datatypes.LOptions.
Require Import Vector.
Inductive term' := var_term' : nat -> term' | Func' (name : nat) | App' : term' -> term' -> term'.
Inductive varornot := isvar | novar.
Inductive wf : varornot -> term' -> Prop :=
| wf_var n : wf isvar (var_term' n)
| wf_fun f : wf novar (Func' f)
| wf_app v s t : wf v s -> wf novar t -> wf novar (App' s t).
Instance max : Signature.
Proof.
unshelve econstructor.
- exact (nat * nat)%type.
- exact (nat * nat)%type.
- exact snd.
- exact snd.
Defined.
Fixpoint to_term (a : list (@Terms.term max)) (t : term') :=
match t with
| var_term' n => var_term n
| Func' n => Func (n, |List.rev a|) (of_list (List.rev a))
| App' s t => to_term (to_term List.nil s :: a) t
end.
Definition mkApps n l (L : Vector.t _ n) := fold_right App' L l.
Fixpoint of_term (t : @Terms.term max) :=
match t with
| var_term n => var_term' n
| Func (n, m) l => mkApps (Func' n) (map of_term l)
end.
Require Import Equations.Prop.DepElim.
Lemma Func_cast F n n' (ts : Vector.t _ n) (ts' : Vector.t _ n') :
forall (H : n = n'), cast ts H = ts' -> Func (F, n) ts = Func (F, n') ts'.
Proof.
intros -> H. f_equal. revert H.
dependent induction ts; cbn; congruence.
Qed.
Lemma Pred_cast P n n' (ts : Vector.t _ n) (ts' : Vector.t _ n') :
forall (H : n = n'), cast ts H = ts' -> Pred (P, n) ts = Pred (P, n') ts'.
Proof.
intros -> H. f_equal. revert H.
dependent induction ts; cbn; congruence.
Qed.
Lemma cast_nil X n (v : Vector.t X n) H :
cast v H = append v VectorDef.nil.
Proof.
induction v; cbn; congruence.
Qed.
Lemma cast_app X n (v : Vector.t X n) (A B : list X) H :
cast (append (of_list (A ++ B)) v) H = append (of_list A) (append (of_list B) v).
Proof.
induction A in B, H |- *; cbn.
- apply cast_eq.
- now rewrite IHA.
Qed.
Lemma to_term_mkApps n k (v : Vector.t Terms.term k) A :
(forall s, vec_in s v -> to_term ([]) (of_term s) = s)
-> to_term A (mkApps (Func' n) (map of_term v))
= Func (n, List.length (List.rev A) + k) (append (of_list (List.rev A)) v).
Proof.
induction v in A |- *; cbn; intros H.
- assert (Heq : | List.rev A | = (| List.rev A |) + 0) by lia.
eapply Func_cast with (H:=Heq). apply cast_nil.
- rewrite IHv; eauto. rewrite H; eauto. cbn.
assert (Heq : (| List.rev A ++ ([h]) |) + n0 = (|List.rev A |) + S n0).
{ rewrite app_length. cbn. lia. }
eapply Func_cast with (H:=Heq). now rewrite cast_app.
Qed.
Lemma to_term_of_term t :
to_term List.nil (of_term t) = t.
Proof.
induction t using strong_term_ind; cbn; trivial.
destruct F. now apply to_term_mkApps.
Qed.
Inductive form' := Fal' | Pred' (P : nat) (args : list term') | Impl' (phi1 phi2 : form') | All' (phi : form').
Fixpoint to_form (f : form') :=
match f with
| Fal' => Fal
| Pred' P L => Pred (P, _) (of_list (List.map (to_term List.nil) L))
| Impl' phi1 phi2 => Impl (to_form phi1) (to_form phi2)
| All' phi => All (to_form phi)
end.
Fixpoint of_form (f : form) :=
match f with
| Fal => Fal'
| Pred (P,_) L => Pred' P (to_list (map of_term L))
| Impl phi1 phi2 => Impl' (of_form phi1) (of_form phi2)
| All phi => All' (of_form phi)
end.
Lemma to_list_length X n (v : Vector.t X n) :
length (to_list v) = n.
Proof.
unfold to_list. induction v; cbn; congruence.
Qed.
Lemma to_form_of_form f :
to_form (of_form f) = f.
Proof.
induction f; cbn; try congruence.
destruct P. cbn. assert (Heq : | [to_term ([]) p | p ∈ to_list (map of_term t)] | = n0).
{ rewrite map_length. apply to_list_length. }
eapply Pred_cast with (H:=Heq). revert Heq. dependent induction t; trivial.
intros H. cbn. f_equal; try apply IHt. apply to_term_of_term.
Qed.
Run TemplateProgram (tmGenEncode "enc_term'" term').
Hint Resolve enc_term'_correct : Lrewrite.
Instance term_var_term': computable var_term'. extract constructor. Qed.
Instance term_Func' : computable Func'. extract constructor. Qed.
Instance term_App' : computable App'. extract constructor. Qed.
Definition App'' '(s,t) := App' t s.
Instance term_App'' : computable App''. extract. Qed.
Fixpoint L_term' n :=
match n with
| 0 => []
| S n => L_term' n ++
List.map var_term' (L_nat n) ++
List.map Func' (L_nat n) ++
List.map App'' (list_prod (L_term' n) (L_term' n))
end.
Instance enum_term' : enumT term'.
Proof.
exists L_term'.
- eauto.
- intros t. induction t.
+ destruct (el_T n) as [m].
exists (1 + m). cbn. in_app 2. eauto.
+ destruct (el_T name) as [m].
exists (1 + m). cbn. in_app 3. eauto.
+ destruct IHt1 as [m1]. destruct IHt2 as [m2].
exists (1 + m1 + m2). cbn. in_app 4. in_collect (t2, t1); eapply cum_ge'; eauto; omega.
Defined.
Require Import List Datatypes.
Instance term_L_term' : computable L_term'. extract. Qed.
Fixpoint L_wf v n :=
match n with
| 0 => []
| S n => L_wf v n ++
match v with
| isvar => List.map var_term' (L_nat n)
| novar => List.map Func' (L_nat n) ++
List.map App'' (list_prod (L_wf novar n) (L_wf novar n)) ++
List.map App'' (list_prod (L_wf novar n) (L_wf isvar n))
end
end.
Run TemplateProgram (tmGenEncode "enc_varornot" varornot).
Hint Resolve enc_varornot_correct : Lrewrite.
Instance term_L_wf : computable L_wf.
Proof.
extract.
Qed.
Lemma enum_wf v : enum (wf v) (L_wf v).
Proof with try (eapply cum_ge'; eauto; omega).
split. eauto.
intros t. split.
- induction 1.
+ destruct (el_T n) as [m]. exists (1 + m). cbn. in_app 2. eauto.
+ destruct (el_T f) as [m]. exists (1 + m). cbn. in_app 2. eauto.
+ destruct (IHwf1) as [m1], (IHwf2) as [m2].
exists (1 + m1 + m2). cbn. destruct v.
* in_app 4. in_collect (t, s)...
* in_app 3. in_collect (t, s)...
- intros [m]. induction m in v, t, H |-*; cbn in *.
+ eauto.
+ inv_collect. destruct v; inv_collect.
* econstructor.
* econstructor.
* econstructor; eauto.
* econstructor; eauto.
Qed.
Run TemplateProgram (tmGenEncode "enc_form'" form').
Hint Resolve enc_form'_correct : Lrewrite.
(* Instance term_Fal' : computable Fal'. extract constructor. Qed. *)
Instance term_Pred' : computable Pred'. extract constructor. Qed.
Instance term_Impl' : computable Impl'. extract constructor. Qed.
Instance term_All' : computable All'. extract constructor. Qed.
Definition Impl'' '(s,t) := Impl' s t.
Instance term_Impl'' : computable Impl''. extract. Qed.
Definition Pred'' '(s,t) := Pred' s t.
Instance term_Pred'' : computable Pred''. extract. Qed.
Definition cons'' : term' * list term' -> list term' := fun '(n, L) => n :: L.
Instance term_cons'' : computable cons''.
Proof.
extract.
Qed.
Definition T_list_term' := @T_list term' _.
Instance term_T_list' : computable T_list_term'.
Proof.
change (computable
(fix T_list (n : nat) : list (list term') :=
match n with
| 0 => [[]]
| S n0 => (T_list n0 ++ List.map cons'' (L_term' n0 × T_list n0))%list
end)).
extract.
Qed.
Fixpoint L_form' n :=
match n with
| 0 => [Fal']
| S n => L_form' n ++
List.map Pred'' (list_prod (L_nat n) (T_list_term' n)) ++
List.map Impl'' (list_prod (L_form' n) (L_form' n)) ++
List.map All' (L_form' n)
end.
Instance term_L_form' : computable L_form'. extract. Qed.
Instance enum_form' : enumT form'.
Proof.
exists L_form'.
- eauto.
- intros t. induction t.
+ exists 0. cbn. eauto.
+ destruct (el_T P) as [m1]. destruct (el_T args) as [m2].
exists (1 + m1 + m2). cbn. in_app 2.
in_collect (P, args); eapply cum_ge'; eauto; omega.
+ destruct IHt1 as [m1]. destruct IHt2 as [m2].
exists (1 + m1 + m2). cbn. in_app 3. in_collect (t1, t2); eapply cum_ge'; eauto; omega.
+ destruct IHt as [m].
exists (1 + m). cbn. in_app 4. eauto.
Defined.
Fixpoint subst_term' (sigmaterm : (fin) -> term' ) (s : term' ) : _ :=
match s with
| var_term' s => sigmaterm s
| Func' f => Func' f
| App' s1 s2 => App' (subst_term' sigmaterm s1) (subst_term' sigmaterm s2)
end.
Fixpoint subst_term'' (b : bool) (sigmaterm : (fin) -> term' ) (s : term' ) : _ :=
match s with
| var_term' s => if b then sigmaterm s else Func' s
| Func' f => Func' f
| App' s1 s2 => App' (subst_term'' true sigmaterm s1) (subst_term'' false sigmaterm s2)
end.
Definition up_term_term' (sigma : (fin) -> term' ) : _ :=
(scons) ((var_term') (var_zero)) ((funcomp) (subst_term' ((funcomp) (var_term' ) (shift))) sigma).
Fixpoint subst_form' (sigmaterm : (fin) -> term' ) (s : form' ) : _ :=
match s with
| Fal' => Fal'
| Pred' P s0 => Pred' P ((List.map (subst_term' sigmaterm)) s0)
| Impl' s0 s1 => Impl' ((subst_form' sigmaterm) s0) ((subst_form' sigmaterm) s1)
| All' s0 => All' ((subst_form' (up_term_term' sigmaterm)) s0)
end.
Definition form_shift' n := var_term' (S n).
Inductive sprvie : list form' -> option form' -> form' -> Prop :=
| ieContr A phi psi : sprvie A (Some phi) psi -> phi el A -> sprvie A None psi
| ieIR A phi psi : sprvie (phi :: A) None psi -> sprvie A None (Impl' phi psi)
| ieAllR A phi : sprvie (List.map (subst_form' form_shift') A) None phi -> sprvie A None (All' phi)
| ieAbsurd A phi : sprvie A None Fal' -> sprvie A None phi
| ieAx A phi : sprvie A (Some phi) phi
| ieIL A phi psi xi : sprvie A None phi -> sprvie A (Some psi) xi -> sprvie A (Some (Impl' phi psi)) xi
| ieAllL A phi v t psi : wf v t -> sprvie A (Some (subst_form' (t .: var_term') phi)) psi -> sprvie A (Some (All' phi)) psi.
Hint Constructors sprvie.
Hint Constructors sprv.
Lemma ext_term' sigma tau phi : (forall x, sigma x = tau x) -> subst_term' sigma phi = subst_term' tau phi.
Proof.
induction phi; cbn; firstorder congruence.
Qed.
Lemma ext_form' sigma tau phi : (forall x, sigma x = tau x) -> subst_form' sigma phi = subst_form' tau phi.
Proof.
induction phi in sigma, tau |- *; cbn; try firstorder congruence.
- intros. f_equal. eapply map_ext. intros; now eapply ext_term'.
- intros. erewrite IHphi1, IHphi2; eauto.
- intros. erewrite IHphi; eauto. intros []; cbn. reflexivity.
unfold funcomp. rewrite H. now eapply ext_term'.
Qed.
Require Import Equations.Prop.DepElim.
Lemma subst_term_of_term sigma t :
subst_term' (sigma >> of_term) (of_term t) = of_term (subst_term sigma t).
Proof.
revert sigma.
induction t using strong_term_ind; cbn; intros.
- reflexivity.
- destruct F. dependent induction v; cbn.
+ reflexivity.
+ rewrite IHv.
* f_equal. apply H. now left.
* intros t Ht sigma'. apply H. now right.
Qed.
Lemma subst_term_map sigma n (t : Vector.t Terms.term n) :
[subst_term' (sigma >> of_term) p | p ∈ to_list (Vector.map of_term t)] =
to_list (Vector.map of_term (Vector.map (subst_term sigma) t)).
Proof.
induction t; cbn; trivial.
now setoid_rewrite IHt; setoid_rewrite subst_term_of_term.
Qed.
Lemma subst_form_of_form sigma phi :
subst_form' (sigma >> of_term) (of_form phi) = of_form (subst_form sigma phi).
Proof.
induction phi in sigma |- *; cbn; try congruence.
- destruct P. cbn. now rewrite subst_term_map.
- f_equal. rewrite <- IHphi.
eapply ext_form'. intros []. cbn. reflexivity. cbn.
now setoid_rewrite <- subst_term_of_term.
Qed.
Lemma wf_of_term t :
{ v | wf v (of_term t)}.
Proof.
induction t using strong_term_ind; cbn.
- exists isvar. econstructor.
- destruct F. exists novar. dependent induction v; cbn in *.
+ econstructor.
+ destruct (X h); eauto. apply (wf_app w). eauto.
Qed.
Lemma of_term_wf' v t :
wf v t -> match v with
| isvar => exists x, t = var_term' x
| novar => exists F n (B : Vector.t Terms.term n), t = of_term (Func (F, n) B)
end.
Proof.
induction 1; cbn.
- exists n. reflexivity.
- exists f, 0, Vector.nil. reflexivity.
- destruct v, IHwf1 as [x Hx], IHwf2 as (f & n & B & Hs); subst.
+ exists f, (S n), (Vector.cons (var_term x) B). reflexivity.
+ destruct Hx as (k & C & ->). exists f, (S n), (Vector.cons (@Func max (x, k) C) B). reflexivity.
Qed.
Lemma of_term_wf v t :
wf v t -> exists t', t = of_term t'.
Proof.
intros H % of_term_wf'. destruct v.
- destruct H as [x ->]. now exists (var_term x).
- destruct H as (f & n & B & ->). eauto.
Qed.
Fixpoint wf_form phi :=
match phi with
| Fal' => True
| Pred' P s0 => forall t, t el s0 -> exists v, wf v t
| Impl' s0 s1 => (wf_form s0) /\ (wf_form s1)
| All' s0 => wf_form s0
end.
Lemma wf_of_form phi :
wf_form (of_form phi).
Proof.
induction phi; cbn; auto. destruct P. cbn.
intros s. rewrite <- Vectors.tolist_In.
intros [s'[<- _]] % Vectors.vect_in_map_iff.
destruct (wf_of_term s'). now exists x.
Qed.
Lemma of_list_wf A :
(forall t, t el A -> exists v, wf v t) -> exists n (ts : Vector.t Terms.term n), A = to_list (Vector.map of_term ts).
Proof.
induction A; cbn; intros H.
- exists 0, Vector.nil. reflexivity.
- destruct IHA as (n & ts & ->); eauto.
destruct (H a) as [v Ha]; auto.
apply of_term_wf in Ha as [t ->].
exists (S n), (Vector.cons t ts). reflexivity.
Qed.
Lemma of_form_wf phi :
wf_form phi -> exists phi', phi = of_form phi'.
Proof.
induction phi; cbn.
- intros _. exists Fal. reflexivity.
- intros H. apply of_list_wf in H as (n & ts & ->).
exists (@Pred max (P, n) ts). reflexivity.
- intros [H1 H2]. destruct (IHphi1 H1) as [phi1' ->], (IHphi2 H2) as [phi2' ->].
exists (Impl phi1' phi2'). reflexivity.
- intros H. destruct (IHphi H) as [phi' ->]. exists (All phi'). reflexivity.
Qed.
Lemma ren_term_to_term xi A t :
to_term (List.map (subst_term (fun n => var_term (xi n))) A) (subst_term' (fun n => var_term' (xi n)) t)
= subst_term (fun n => var_term (xi n)) (to_term A t).
Proof.
induction t in A |- *; cbn; try firstorder congruence.
- rewrite <- map_rev.
assert (H : |([subst_term (make_subst xi) p | p ∈ List.rev A])| = |List.rev A|) by now rewrite map_length.
eapply Func_cast with (H:=H). induction (List.rev A); cbn; trivial. now rewrite IHl.
- setoid_rewrite (IHt1 List.nil). rewrite <- IHt2. reflexivity.
Qed.
Lemma ren_term_to_term' xi t :
to_term ([]) (subst_term' (fun n => var_term' (xi n)) t)
= subst_term (fun n => var_term (xi n)) (to_term ([]) t).
Proof.
now rewrite <- ren_term_to_term.
Qed.
Lemma ren_form_to_form xi phi :
to_form (subst_form' (fun n => var_term' (xi n)) phi) = subst_form (fun n => var_term (xi n)) (to_form phi).
Proof.
induction phi in xi |- *; cbn; trivial.
- assert (H : |[to_term ([]) p | p ∈ [subst_term' (fun n => var_term' (xi n)) p | p ∈ args]]|
= |[to_term ([]) p | p ∈ args]|) by now rewrite !map_length.
eapply Pred_cast with (H:=H). induction args in H |- *; cbn; trivial.
rewrite IHargs. now rewrite ren_term_to_term'.
- now rewrite IHphi1, IHphi2.
- f_equal. unfold up_term_term'.
specialize (IHphi (fun n => match n with 0 => 0 | S n => S (xi n) end)).
erewrite ext_form.
+ rewrite <- IHphi. f_equal. apply ext_form'. now intros [].
+ now intros [].
Qed.
Definition option_pred X (p : X -> Prop) (x : option X) :=
match x with
| Some x => p x
| None => True
end.
Lemma prvie_prv' A psi phi :
(forall theta, theta el A -> wf_form theta) -> option_pred wf_form psi -> wf_form phi ->
sprvie A psi phi -> sprv expl (List.map to_form A) (option_map to_form psi) (to_form phi).
Proof.
intros H1 H2 H3.
induction 1; cbn in *; eauto; subst.
- apply (Contr (phi:=to_form phi)); eauto.
- destruct H3. apply IR, IHsprvie; trivial.
intros theta [-> | HT]; auto.
- eapply AllR. rewrite map_map in *. erewrite map_ext.
+ apply IHsprvie; trivial. intros theta [theta' [<- HT]] % in_map_iff.
destruct (of_form_wf (H1 theta' HT)) as [psi ->].
rewrite (ext_form' (tau:= form_shift >> of_term)); try now intros x.
rewrite subst_form_of_form. apply wf_of_form.
+ intros theta. cbn. now setoid_rewrite ren_form_to_form.
- apply IL; firstorder.
- apply AllL with (t0:=to_term List.nil t).
assert (exists t', t = of_term t') as [t' ->] by now eapply of_term_wf.
assert (exists phi', phi = of_form phi') as [phi' ->] by now apply of_form_wf.
rewrite to_term_of_term, to_form_of_form.
erewrite ext_form' in IHsprvie.
+ erewrite subst_form_of_form, to_form_of_form in IHsprvie.
apply IHsprvie; trivial. apply wf_of_form.
+ intros x. asimpl. now destruct x.
Qed.
Lemma option_map_id A (f : A -> A) o :
(forall x, f x = x) -> option_map f o = o.
Proof.
destruct o; cbn.
- intros. now rewrite H.
- reflexivity.
Qed.
Lemma option_map_map A B C (f : A -> B) (g : B -> C) o :
option_map g (option_map f o) = option_map (f >> g) o.
Proof.
destruct o; cbn.
- intros. reflexivity.
- reflexivity.
Qed.
Lemma prvie_prv A psi phi :
sprvie (List.map of_form A) (option_map of_form psi) (of_form phi) -> sprv expl A psi phi.
Proof.
intros H % prvie_prv'.
- rewrite to_form_of_form, map_map in H.
erewrite map_ext in H. 2: eapply to_form_of_form.
rewrite map_id, option_map_map, option_map_id in H; trivial.
eauto using to_form_of_form.
- intros H [phi'[<- _]] % in_map_iff. apply wf_of_form.
- destruct psi; cbn; trivial. apply wf_of_form.
- apply wf_of_form.
Qed.
Lemma prv_prvie A psi phi :
sprv expl A psi phi -> sprvie (List.map of_form A) (option_map of_form psi) (of_form phi).
Proof.
induction 1; cbn in *; eauto.
- eapply ieAllR. rewrite map_map in *.
erewrite map_ext. eassumption.
intros; cbn. rewrite <- subst_form_of_form.
eapply ext_form'. reflexivity.
- destruct (wf_of_term t). eapply ieAllL. eassumption. setoid_rewrite <- subst_form_of_form in IHsprv.
erewrite ext_form'. eassumption. intros []; reflexivity.
Qed.
Import ListNotations.
Instance HdF : eq_dec Funcs.
Proof.
cbn. exact _.
Qed.
Instance HdP : eq_dec Preds.
Proof.
cbn. exact _.
Qed.
Instance HeF : enumT Funcs.
Proof.
cbn. exact _.
Qed.
Instance HeP : enumT Preds.
Proof.
cbn. exact _.
Qed.
Require Import Undecidability.L.Datatypes.LNat Nat.
Fixpoint term_eqb (t1 t2 : term') :=
match t1, t2 with
| var_term' n, var_term' m => eqb n m
| Func' f1, Func' f2 => eqb f1 f2
| App' t1 t2, App' t1' t2' => andb (term_eqb t1 t1') (term_eqb t2 t2')
| _, _ => false
end.
Lemma term_eqb_spec t1 t2 : reflect (t1 = t2) (term_eqb t1 t2).
Proof.
induction t1 in t2 |- *; destruct t2; cbn.
all: try now econstructor; congruence.
- destruct (Nat.eqb_spec n n0); econstructor; congruence.
- destruct (Nat.eqb_spec name name0); econstructor; congruence.
- destruct (IHt1_1 t2_1), (IHt1_2 t2_2).
all: try now econstructor; congruence.
Qed.
Instance computable_term_eqb : computable term_eqb.
Proof.
extract.
Qed.
Definition list_term_eqb := list_eqb term_eqb.
Fixpoint form_eqb (t1 t2 : form') :=
match t1, t2 with
| Pred' p1 L1, Pred' p2 L2 => andb (Nat.eqb p1 p2) (list_term_eqb L1 L2)
| Fal', Fal' => true
| Impl' t1 t2, Impl' t1' t2' => andb (form_eqb t1 t1') (form_eqb t2 t2')
| All' phi1, All' phi2 => form_eqb phi1 phi2
| _, _ => false
end.
Lemma form_eqb_spec t1 t2 : reflect (t1 = t2) (form_eqb t1 t2).
Proof.
induction t1 in t2 |- *; destruct t2; cbn.
all: unfold list_term_eqb in *.
all: try now econstructor; congruence.
- destruct (Nat.eqb_spec P P0), (list_eqb_spec term_eqb_spec args args0).
all: econstructor; congruence.
- destruct (IHt1_1 t2_1), (IHt1_2 t2_2); econstructor; congruence.
- destruct (IHt1 t2); econstructor; congruence.
Qed.
Instance computable_list_eqb : computable list_term_eqb.
Proof.
unfold list_term_eqb.
extract.
Qed.
Instance computable_form_eqb : computable form_eqb.
Proof.
extract.
Qed.
Definition list_form_eqb := list_eqb form_eqb.
Definition option_form_eqb := option_eqb form_eqb.
Instance computable_list_form_eqb : computable list_form_eqb.
Proof.
unfold list_form_eqb.
extract.
Qed.
Instance computable_option_form_eqb : computable option_form_eqb.
Proof.
unfold option_form_eqb.
extract.
Qed.
Definition enum_eqb : (list form' * option form' * form' * (list form' * option form' * form')) -> bool := fun '(A, psi, phi, (A', psi', phi')) => list_form_eqb A A' && option_form_eqb psi psi' && form_eqb phi phi'.
Instance computable_enum_eqb : computable enum_eqb.
Proof.
extract.
Qed.
(* Instance test : eq_dec form'. *)
(* Proof. *)
(* intros ? ?. hnf. repeat decide equality. *)
(* Qed. *)
Definition f1 := (fun L_seq : list form' -> option form' -> list form' => fun A => fun phi : form' =>
List.map (Impl' phi) (L_seq (Datatypes.cons phi A) None)).
Instance term_f1 : computable f1.
Proof.
extract.
Qed.
Definition f2 ( L_seq : option form' -> list form') := (fun psi0 : form' => L_seq (Some psi0) ).
Instance term_f2 : computable f2.
Proof.
extract.
Qed.
Definition in_eqb a := existsb (form_eqb a).
Instance term_existsb : computable (@existsb form').
Proof.
extract.
Qed.
Instance computable_ineqb : computable in_eqb.
Proof.
extract.
Qed.
Lemma in_eqb_spec a L : reflect (List.In a L) (in_eqb a L).
Proof.
pose proof (existsb_exists (form_eqb a) L).
unfold in_eqb.
destruct (existsb (form_eqb a) L).
- econstructor. destruct H as [? _]. destruct (H eq_refl) as (? & ? & ?).
eapply (reflect_iff _ _ (form_eqb_spec a x)) in H1. subst. eauto.
- econstructor. intros ?. destruct H as [_ ?].
enough (false = true) by congruence.
eapply H. exists a. split. eauto.
eapply (reflect_iff _ _ (form_eqb_spec a a)). eauto.
Qed.
Definition f3 ( L_seq : option form' -> list form') :=
(fun _ : form' => in_eqb Fal' (L_seq None )).
Instance term_f3 : computable f3.
Proof.
extract.
Qed.
Definition f4 ( L_seq : option form' -> list form') phi :=
(fun _ : form' => in_eqb phi (L_seq None )).
Instance term_f4 : computable f4.
Proof.
extract.
Qed.
Definition f5 ( L_seq : option form' -> list form') psi :=
(fun t : term' =>
(L_seq (Some (subst_form' (scons t var_term') psi )) )).
Instance term_scons : computable (@scons term').
Proof.
extract.
Qed.
Instance term_subst_term' : computable subst_term'.
Proof.
extract.
Qed.
Definition f6 := (funcomp var_term' shift).
Instance term_f6 : computable f6.
Proof.
unfold f6, funcomp, shift. extract.
Qed.
Definition f7 (sigma : nat -> term') := sigma >> subst_term' f6.
Instance term_f7 : computable f7.
Proof.
unfold f7, funcomp, shift. extract.
Qed.
Instance term_up_term_term' : computable up_term_term'.
Proof.
unfold up_term_term'. unfold var_zero.
change (computable (fun sigma : fin -> term' => var_term' 0 .: f7 sigma)).
unfold scons.
extract.
Qed.
Instance term_subst_form' : computable subst_form'.
Proof.
unfold subst_form'.
extract. Unshelve. 3:{
split. Lrewrite_generateGoals. 1-5:reflexivity.
lazymatch goal with
|- ?s >* ?t =>
is_ground s;
let IH := fresh "IH" in
unshelve epose (IH:=_);[|(notypeclasses refine (_:{v:L.term & computesExp _ _ s v})); solve [shelve]|];
let v := constr:(projT1 IH) in
assert (IHR := fst (projT2 IH));
let IHInts := constr:( snd (projT2 IH)) in
lazymatch type of IHInts with
computes ?ty _ ?v =>
change v with (@ext _ ty _ (Build_computable IHInts)) in IHR;exact (proj1 IHR)
end
end.
Unshelve.
6: eapply IHP; eauto.
Unshelve. 4:{
eapply extCorrect. }
Lrewrite. reflexivity. Lproc. }
Intern.cstep.
Qed.
Instance term_f5 : computable f5.
Proof.
unfold f5. extract.
Qed.
Instance term_form_shift' : computable form_shift'.
Proof.
extract.
Qed.
Require Import List Datatypes.
Fixpoint L_seq n (A : list form') (psi : option form') : list form' :=
match n with
| 0 => match psi with Some psi => [psi] | None => A end
| S n => L_seq n A psi ++
match psi with
(* Contr *) | None => (concat (List.map (f2 (L_seq n A)) A)) ++
(* IR *) (concat
(List.map
(f1 (L_seq n) A)
(L_form' n ))) ++
(* AllR *) (List.map All'
(L_seq n (List.map (subst_form' form_shift') A) None )) ++
(* Absurd *) (filter (f3 (L_seq n A)) (L_form' n ))
(* IL *) | Some (Impl' phi psi) => (filter (f4 (L_seq n A) phi) (L_seq n A (Some psi ) ))
(* AllL *) | Some (All' psi) => concat
(List.map
(f5 (L_seq n A) psi)
(L_wf isvar n )) ++ concat
(List.map
(f5 (L_seq n A) psi)
(L_wf novar n ))
| _ => []
end
end.
(* Instance term_concat : computable (@concat form'). *)
(* Proof. *)
(* extract. *)
(* Qed. *)
Instance term_L_seq : computable L_seq.
Proof.
extract.
Qed.
Opaque in_dec.
Lemma bool_true_Prop: forall b : bool, b -> b = true.
Proof.
destruct b; firstorder.
Qed.
Lemma enum_sprv A psi : enum (sprvie A psi) (fun n => L_seq n A psi).
Proof with try (eapply cum_ge' with (L := fun n => L_seq n _ _ ); eauto; omega); try (eapply cum_ge'; eauto; omega).
repeat split.
- eauto.
- rename x into phi. induction 1; try congruence; subst.
all: unfold f1, f2, f3, f4, f5 in *.
+ destruct IHsprvie as [m]. exists (S m). cbn. in_app 2.
eapply in_concat_iff. eexists. split. 2: in_collect phi... all: eauto.
+ destruct IHsprvie as [m1], (el_T phi) as [m2]. exists (1 + m1 + m2). cbn. in_app 3.
eapply in_concat_iff. eexists. split. 2: in_collect phi... in_collect psi...
+ destruct IHsprvie as [m]. exists (S m). cbn. in_app 4. in_collect phi...
+ destruct IHsprvie as [m1], (el_T phi) as [m2]. exists (1 + m1 + m2). cbn. in_app 5.
match goal with [ |- _ el filter _ _ ] => eapply in_filter_iff; split; [ try (rewrite !in_prod_iff; repeat split) | ] | _ => try (rewrite !in_prod_iff; repeat split) end...
eapply bool_Prop_true.
rewrite <- reflect_iff. 2:eapply in_eqb_spec. idtac...
+ exists 0. now left.
+ destruct IHsprvie1 as [m1], IHsprvie2 as [m2]. exists (1 + m1 + m2). cbn. in_app 2. match goal with [ |- _ el filter _ _ ] => eapply in_filter_iff; split; [ try (rewrite !in_prod_iff; repeat split) | ] | _ => try (rewrite !in_prod_iff; repeat split) end...
eapply bool_Prop_true.
rewrite <- reflect_iff. 2:eapply in_eqb_spec. idtac...
+ eapply enum_wf in H. destruct IHsprvie as [m1], H as [m2]. exists (1 + m1 + m2). cbn.
destruct v.
* in_app 2. eapply in_concat_iff.
eexists. split. 2: in_collect t... unfold f5. idtac...
* in_app 3. eapply in_concat_iff.
eexists. split. 2: in_collect t... unfold f5. idtac...
- intros [m]. induction m in A, psi, x, H |-*; destruct psi; cbn in *.
+ destruct H as [-> | []]. apply ieAx.
+ eauto.
+ unfold f1, f2, f3, f4, f5 in *.
Ltac inv_collect :=
repeat
(match goal with
| [ H : ?x el concat _ |- _ ] => eapply in_concat_iff in H as (? & ? & ?)
| [ H : ?x el List.map _ _ |- _ ] => eapply in_map_iff in H as (? & ? & ?)
| [ x : ?A * ?B |- _ ] => destruct x; subst
| [ H : ?x el filter _ _ |- _ ] => let H' := fresh "H" in eapply in_filter_iff in H as (? & H')
| [ H : ?x el list_prod _ _ |- _ ] => eapply in_prod_iff in H
| [ H : _ el _ ++ _ |- _ ] => try eapply in_app_iff in H as []
| [H : _ el _ :: _ |- _ ] => destruct H
end; subst).
destruct f; inv_collect; eauto.
* eapply bool_true_Prop in H0. rewrite <- reflect_iff in H0. 2: eapply in_eqb_spec.
eauto.
* econstructor. 2: eauto. eapply enum_wf. eauto.
* econstructor. 2: eauto. eapply enum_wf. eauto.
+ unfold f1, f2, f3, f4, f5 in *.
inv_collect; eauto. destruct (in_eqb_spec Fal' (L_seq m A None)).
eauto. firstorder.
Qed.
Definition T_form_term' := @T_list form' _.
Definition cons''' : form' * list form' -> list form' := fun '(n, L) => n :: L.
Instance term_cons''' : computable cons'''.
Proof.
extract.
Qed.
Instance term_T_form' : computable T_form_term'.
Proof.
change (computable
(fix T_list (n : nat) : list (list form') :=
match n with
| 0 => [[]]
| S n0 => (T_list n0 ++ List.map cons''' (L_form' n0 × T_list n0))%list
end)).
extract.
Qed.
Definition f8 (L_seq : list form' -> option form' -> list form') := fun '(A, psi, phi) => in_eqb phi (L_seq A psi).
Instance computable_f8 : computable f8.
Proof.
extract.
Qed.
Definition f9 (L_seq : list form' -> option form' -> list form') : list form' * option form' * _ -> bool := fun '(A, psi, phi) => in_eqb phi (L_seq A None).
Instance computable_f9 : computable f9.
Proof.
extract.
Qed.
Fixpoint L_sprvie n :=
match n with
| 0 => []
| S n => L_sprvie n ++
List.filter (f8 (L_seq n)) (list_prod (list_prod (T_form_term' n) (List.map Some (L_form' n))) (L_form' n)) ++
List.filter (f9 (L_seq n)) (list_prod (list_prod (T_form_term' n) (List.cons (@None form') List.nil)) (L_form' n))
end.
Instance computable_L_sprvie : computable L_sprvie.
Proof.
extract.
Qed.
Lemma enum_sprvie : enum (fun '(A, psi, phi) => sprvie A psi phi) L_sprvie.
Proof with try (eapply cum_ge'; eauto; omega).
repeat split.
- eauto.
- destruct x as [[A psi] phi]. intros.
destruct (el_T A) as [m1].
destruct (el_T phi) as [m2].
eapply enum_sprv in H as [m3].
destruct psi as [psi| ].
+ destruct (el_T psi) as [m4].
exists (1 + m1 + m2 + m3 + m4).
cbn. in_app 2.
eapply in_filter_iff. split.
rewrite !in_prod_iff. repeat split...
eapply in_map_iff. repeat esplit; eauto...
unfold f8.
Set Printing Coercions. eapply bool_Prop_true.
rewrite <- reflect_iff. 2:eapply in_eqb_spec.
eapply cum_ge' with (L := (fun n => L_seq n A (Some psi))); eauto; omega.
+ exists (1 + m1 + m2 + m3).
cbn. in_app 3.
eapply in_filter_iff. split.
rewrite !in_prod_iff. repeat split... firstorder.
unfold f9.
Set Printing Coercions. eapply bool_Prop_true.
rewrite <- reflect_iff. 2:eapply in_eqb_spec.
eapply cum_ge' with (L := (fun n => L_seq n A None)); eauto; omega.
- intros [m Hm]. destruct x as [[A psi] phi].
induction m in A, psi, phi, Hm |- *; cbn in *.
+ firstorder.
+ unfold f8, f9 in *. inv_collect; eauto.
* eapply bool_true_Prop in H0. rewrite <- reflect_iff in H0. 2: eapply in_eqb_spec.
eapply enum_sprv. eauto.
* eapply bool_true_Prop in H0. rewrite <- reflect_iff in H0. 2: eapply in_eqb_spec.
destruct H. eapply list_prod_in in H as (? & ? & ? & ? & ?). symmetry in H. inv H. subst.
destruct H3 as [<- | []].
eapply enum_sprv. eauto.
Qed.