Lemma flat_map_app {X Y} A B (f : X -> list Y) :
flat_map f (A ++ B) = flat_map f A ++ flat_map f B.
Proof.
induction A; cbn.
- reflexivity.
- now rewrite IHA, app_assoc.
Qed.
Lemma switch_map {X Y} (P : Y -> Prop) (f : X -> Y) A :
(forall x, x el A -> P (f x)) -> forall y, y el (map f A) -> P y.
Proof.
intros H y (x & <- & Hx) % in_map_iff. eauto.
Qed.
Fixpoint at_pos {X} n x (A : list X) :=
match A with
| nil => False
| a :: A' =>
match n with
| O => a = x
| S n' => at_pos n' x A'
end
end.
Lemma el_at_pos {X} x (A : list X) :
x el A <-> exists n, at_pos n x A.
Proof.
induction A.
- split. intuition. intros [ [] [] ].
- split.
+ intros [-> | H].
* now exists 0.
* apply IHA in H as [n H']. now exists (S n).
+ intros [ [] H].
* now left.
* right. apply IHA. now exists n.
Qed.
Section L_T_unused.
Context {Sigma : Signature}.
Hypothesis enum_Funcs : enumT Funcs.
Hypothesis enum_Preds : enumT Preds.
Lemma L_T_nat_le n m :
n el L_T m -> n <= m.
Proof.
induction m.
- intros []; now subst.
- intros [ | [ | [] ] ] % in_app_or.
+ constructor. now apply IHm.
+ now subst.
Qed.
Lemma L_T_unused_t n m t :
m <= n -> t el (L_T m) -> unused_term n t.
Proof.
revert n t. induction m; intros n t.
- inversion 1; cbn; tauto.
- intros H [ | [ | (A & H0 & (f & <- & Hf) % in_map_iff) % in_concat_iff ]] % in_app_or.
* apply IHm. omega. assumption.
* subst. constructor. omega.
* revert H0. apply switch_map. intros v H'. rewrite <- vecs_from_correct in H'. constructor.
intros s Hs % H'. apply IHm. 1: omega. assumption.
Qed.
Lemma L_T_unused_v n m k (v : Vector.t term k) :
m <= n -> v el (L_T m) -> (forall t, vec_in t v -> unused_term n t).
Proof.
induction m; intros Hnm.
- intros [].
- cbn. intros [ | H ] % in_app_or.
+ firstorder.
+ rewrite <- vecs_from_correct in H. intros t Ht. apply L_T_unused_t with m. all: omega + eauto.
Qed.
Lemma L_T_unused n m phi :
m <= n -> phi el (L_T m) -> unused n phi.
Proof.
revert n phi. induction m; intros n phi.
- intros ? [<- | []]. constructor.
- intros H [ | [ | [ | [ (A & H0 & (P & <- & HP) % in_map_iff) % in_concat_iff | [] % in_app_or ] % in_app_or] % in_app_or]] % in_app_or;
try (revert H0; apply switch_map).
+ apply IHm. omega. assumption.
+ subst. constructor.
+ contradiction H0.
+ intros v H'. constructor. intros. apply L_T_unused_v with m (pred_ar P) v. all: omega + eauto.
+ intros [phi1 phi2] [] % in_prod_iff. constructor.
all: apply IHm; [omega | assumption].
+ intros psi H'. constructor. apply IHm. omega. assumption.
Qed.
End L_T_unused.
Section Enumeration.
Variable X : Type.
Context {Henum : enumT X}.
Context {Hdec : eq_dec X}.
Hypothesis Hlen : forall n, | L_T n | > n.
Definition plain_enum n : X := proj1_sig (@nthe_length X (L_T n) n (Hlen n)).
Lemma L_T_sub n m :
n <= m -> exists A, L_T m = L_T n ++ A.
Proof.
induction 1.
- exists nil. now rewrite app_nil_r.
- destruct IHle as [A HA]. destruct (cum_T m) as [B HB].
exists (A ++ B). now rewrite HB, HA, app_assoc.
Qed.
Lemma L_T_sub_or n m :
(exists A, L_T n = L_T m ++ A) \/ (exists A, L_T m = L_T n ++ A).
Proof.
destruct (Nat.le_ge_cases n m) as [Hl | Hl]; [right | left]; now apply L_T_sub.
Qed.
Lemma plain_enum_enumerates x :
exists n, plain_enum n = x.
Proof.
destruct (el_T x) as [m H]. destruct (el_pos Hdec H) as [n H'].
exists n. unfold plain_enum. destruct (nthe_length (Hlen n)) as [y H'']. cbn.
apply pos_nthe in H'. destruct (L_T_sub_or n m) as [ [A HA] | [A HA] ].
- rewrite HA in H''. apply (nthe_app_l A) in H'. congruence.
- rewrite HA in H'. apply (nthe_app_l A) in H''. congruence.
Qed.
Lemma plain_enum_slow n :
plain_enum n el L_T n.
Proof.
unfold plain_enum. destruct (nthe_length (Hlen n)) as [y H'']. cbn. now apply nth_error_In in H''.
Qed.
End Enumeration.
Section L_T_Enumeration.
Context {Sigma : Signature}.
Context {HdF : eq_dec Funcs} {HdP : eq_dec Preds}.
Context {HeF : enumT Funcs} {HeP : enumT Preds}.
Lemma L_T_form_len n :
| L_T form n | > n.
Proof.
induction n; cbn.
- omega.
- rewrite app_length. cbn. change (L_T n) with (L_form HeF HeP n) in IHn. omega.
Qed.
Definition form_enum n := plain_enum L_T_form_len n.
Corollary form_enum_enumerates x :
exists n, form_enum n = x.
Proof. apply plain_enum_enumerates. intuition. Qed.
Lemma form_enum_fresh n m :
n <= m -> unused m (form_enum n).
Proof.
intros H. apply (@L_T_unused _ _ _ m n). exact H.
apply plain_enum_slow.
Qed.
End L_T_Enumeration.