-
Notifications
You must be signed in to change notification settings - Fork 0
/
termsyntax.v
75 lines (59 loc) · 4.38 KB
/
termsyntax.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
Require Export unscoped header_extensible.
Class Signature := B_S { Funcs : Type; fun_ar : Funcs -> nat ; Preds : Type; pred_ar : Preds -> nat }.
Section term.
Context {Sigma : Signature}.
Inductive term : Type :=
| var_term : ( fin ) -> term
| Func : forall (f : Funcs), ( vect term (fun_ar f) ) -> term .
Lemma congr_Func { f : Funcs } { s0 : vect term (fun_ar f) } { t0 : vect term (fun_ar f) } (H1 : s0 = t0) : Func f s0 = Func f t0 .
Proof. congruence. Defined.
Fixpoint subst_term (sigmaterm : ( fin ) -> term ) (s : term ) : term :=
match s return term with
| var_term s => sigmaterm s
| Func f s0 => Func f (vect_map (subst_term sigmaterm) s0)
end.
Definition up_term_term (sigma : ( fin ) -> term ) : ( fin ) -> term :=
(scons) ((var_term ) (var_zero)) ((funcomp) (subst_term ((funcomp) (var_term ) (shift))) sigma).
Definition upId_term_term (sigma : ( fin ) -> term ) (Eq : forall x, sigma x = (var_term ) x) : forall x, (up_term_term sigma) x = (var_term ) x :=
fun n => match n with
| S fin_n => (ap) (subst_term ((funcomp) (var_term ) (shift))) (Eq fin_n)
| 0 => eq_refl
end.
Fixpoint idSubst_term (sigmaterm : ( fin ) -> term ) (Eqterm : forall x, sigmaterm x = (var_term ) x) (s : term ) : subst_term sigmaterm s = s :=
match s return subst_term sigmaterm s = s with
| var_term s => Eqterm s
| Func f s0 => congr_Func ((vect_id (idSubst_term sigmaterm Eqterm)) s0)
end.
Definition upExt_term_term (sigma : ( fin ) -> term ) (tau : ( fin ) -> term ) (Eq : forall x, sigma x = tau x) : forall x, (up_term_term sigma) x = (up_term_term tau) x :=
fun n => match n with
| S fin_n => (ap) (subst_term ((funcomp) (var_term ) (shift))) (Eq fin_n)
| 0 => eq_refl
end.
(*
Fixpoint ext_term (sigmaterm : ( fin ) -> term ) (tauterm : ( fin ) -> term ) (Eqterm : forall x, sigmaterm x = tauterm x) (s : term ) : subst_term sigmaterm s = subst_term tauterm s :=
match s return subst_term sigmaterm s = subst_term tauterm s with
| var_term s => Eqterm s
| Func f s0 => congr_Func ((vect_ext (ext_term sigmaterm tauterm Eqterm)) s0)
end.
*)
Fixpoint compSubstSubst_term (sigmaterm : ( fin ) -> term ) (tauterm : ( fin ) -> term ) (thetaterm : ( fin ) -> term ) (Eqterm : forall x, ((funcomp) (subst_term tauterm) sigmaterm) x = thetaterm x) (s : term ) : subst_term tauterm (subst_term sigmaterm s) = subst_term thetaterm s :=
match s return subst_term tauterm (subst_term sigmaterm s) = subst_term thetaterm s with
| var_term s => Eqterm s
| Func f s0 => congr_Func ((vect_comp (compSubstSubst_term sigmaterm tauterm thetaterm Eqterm)) s0)
end.
Definition up_subst_subst_term_term (sigma : ( fin ) -> term ) (tauterm : ( fin ) -> term ) (theta : ( fin ) -> term ) (Eq : forall x, ((funcomp) (subst_term tauterm) sigma) x = theta x) : forall x, ((funcomp) (subst_term (up_term_term tauterm)) (up_term_term sigma)) x = (up_term_term theta) x :=
fun n => match n with
| S fin_n => (eq_trans) (compSubstSubst_term ((funcomp) (var_term ) (shift)) (up_term_term tauterm) ((funcomp) (up_term_term tauterm) (shift)) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstSubst_term tauterm ((funcomp) (var_term ) (shift)) ((funcomp) (subst_term ((funcomp) (var_term ) (shift))) tauterm) (fun x => eq_refl) (sigma fin_n))) ((ap) (subst_term ((funcomp) (var_term ) (shift))) (Eq fin_n)))
| 0 => eq_refl
end.
(*
Lemma instId_term : subst_term (var_term ) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_term (var_term ) (fun n => eq_refl) ((id) x))). Qed.
Lemma varL_term (sigmaterm : ( fin ) -> term ) : (funcomp) (subst_term sigmaterm) (var_term ) = sigmaterm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.
Lemma compComp_term (sigmaterm : ( fin ) -> term ) (tauterm : ( fin ) -> term ) (s : term ) : subst_term tauterm (subst_term sigmaterm s) = subst_term ((funcomp) (subst_term tauterm) sigmaterm) s .
Proof. exact (compSubstSubst_term sigmaterm tauterm (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_term (sigmaterm : ( fin ) -> term ) (tauterm : ( fin ) -> term ) : (funcomp) (subst_term tauterm) (subst_term sigmaterm) = subst_term ((funcomp) (subst_term tauterm) sigmaterm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_term sigmaterm tauterm n)). Qed.
*)
End term.