Commit 65eabe25 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Mix : height of term and formula (disseminated elsewhere earlier)

parent 69ef3de6
......@@ -376,13 +376,6 @@ Proof.
now rewrite decode_code_pair.
Qed.
Fixpoint term_height t :=
match t with
| FVar _ => 0
| BVar _ => 0
| Fun _ l => S (list_max (map term_height l))
end.
Fixpoint code_hterm t :=
match t with
| FVar v => code_pair (0, string_index v)
......@@ -449,14 +442,6 @@ Proof.
apply (countable_by_inverse _ _ decode_code_term).
Qed.
Fixpoint form_height f :=
match f with
| True | False | Pred _ _ => 0
| Not f => S (form_height f)
| Op _ f1 f2 => S (Nat.max (form_height f1) (form_height f2))
| Quant _ f => S (form_height f)
end.
Definition code_op o :=
match o with
| And => 4
......@@ -522,14 +507,14 @@ Fixpoint decode_hform h n :=
end.
Definition code_form f :=
code_pair (S (form_height f), code_hform f).
code_pair (S (height f), code_hform f).
Definition decode_form n :=
let (h,m) := decode_pair n in
decode_hform h m.
Lemma decode_code_hform h f :
form_height f < h -> decode_hform h (code_hform f) = f.
height f < h -> decode_hform h (code_hform f) = f.
Proof.
revert f.
induction h as [|h IH].
......
......@@ -978,3 +978,35 @@ Instance form_fclosed : IsFClosed formula :=
| Op _ f1 f2 => form_fclosed f1 &&& form_fclosed f2
| Quant _ f => form_fclosed f
end.
(** The height of a term (used in Countable.v) *)
Fixpoint term_height t :=
match t with
| FVar _ => 0
| BVar _ => 0
| Fun _ l => S (list_max (map term_height l))
end.
(** The height of a formula (for some non-structural inductions,
also used in Countable.v) *)
Fixpoint height f :=
match f with
| True | False | Pred _ _ => 0
| Not f => S (height f)
| Op _ f1 f2 => S (Nat.max (height f1) (height f2))
| Quant _ f => S (height f)
end.
Lemma height_ind (P : formula -> Prop) :
(forall h, (forall f, height f < h -> P f) ->
(forall f, height f < S h -> P f)) ->
forall f, P f.
Proof.
intros IH f.
set (h := S (height f)).
assert (LT : height f < h) by (cbn; auto with * ).
clearbody h. revert f LT.
induction h as [|h IHh]; [inversion 1|eauto].
Qed.
......@@ -358,34 +358,6 @@ Proof.
eapply R_Not_e; [apply R'_Ax|]. now apply Pr_pop.
Qed.
Fixpoint height f :=
match f with
| True | False | Pred _ _ => 0
| Not f => S (height f)
| Op _ f1 f2 => S (Nat.max (height f1) (height f2))
| Quant _ f => S (height f)
end.
Lemma height_bsubst n t f :
height (bsubst n t f) = height f.
Proof.
revert n t.
induction f; cbn; f_equal; auto.
Qed.
Lemma height_ind (P : formula -> Prop) :
(forall h, (forall f, height f < h -> P f) ->
(forall f, height f < S h -> P f)) ->
forall f, P f.
Proof.
intros IH f.
set (h := S (height f)).
assert (LT : height f < h) by (cbn; auto with * ).
clearbody h. revert f LT.
induction h as [|h IHh]; [inversion 1|eauto].
Qed.
Lemma interp_carac A : WF th A ->
forall G, finterp mo G [] A <-> IsTheorem K th (closure G A).
Proof.
......
......@@ -443,6 +443,14 @@ Proof.
- intros [= <- E]. f_equal. eapply IHf; eauto.
Qed.
(** [bsubst] preserves formula's height *)
Lemma height_bsubst n t f :
height (bsubst n t f) = height f.
Proof.
revert n t. induction f; cbn; f_equal; auto.
Qed.
(** ** Part 3 : properties of [fclosed] *)
Lemma term_fclosed_spec t : fclosed t = true <-> FClosed t.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment