(*
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
Require Import List Lia.
Import ListNotations.
Require Import Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped.
Import UnscopedNotations.
Require Import Undecidability.SystemF.Util.Facts Undecidability.SystemF.Util.poly_type_facts.
Require Import ssreflect ssrbool ssrfun.
Set Default Goal Selector "!".
(* evaluates predicate p on all free variables *)
Fixpoint allfv_pure_term (p: nat -> Prop) (M: pure_term) :=
match M with
| pure_var x => p x
| pure_app M N => allfv_pure_term p M /\ allfv_pure_term p N
| pure_abs M => allfv_pure_term (scons True p) M
end.
Lemma allfv_pure_term_impl {p1 p2: nat -> Prop} {M}:
(forall x, p1 x -> p2 x) -> allfv_pure_term p1 M -> allfv_pure_term p2 M.
Proof.
elim: M p1 p2.
- move=> >. by apply.
- by move=> ? IH1 ? IH2 > /= /copy [/IH1 {}IH1 /IH2 {}IH2] [/IH1 ? /IH2 ?].
- move=> > IH > H /=. apply: IH. by case.
Qed.
Lemma allfv_pure_term_ren_pure_term {p ξ M} :
allfv_pure_term p (ren_pure_term ξ M) <-> allfv_pure_term (ξ >> p) M.
Proof.
elim: M ξ p.
- done.
- move=> ? IH1 ? IH2 > /=. by rewrite IH1 IH2.
- move=> ? IH > /=. rewrite IH. constructor; apply: allfv_pure_term_impl; by case.
Qed.
Lemma allfv_pure_term_TrueI {p: nat -> Prop} {M} : (forall x, p x) -> allfv_pure_term p M.
Proof.
move=> Hp. elim: M.
- move=> > /=. by apply: Hp.
- by move=> ? + ? + /=.
- move=> ? /=. apply: allfv_pure_term_impl. case; first done.
move=> *. by apply: Hp.
Qed.
Lemma ren_pure_term_id {M} : ren_pure_term id M = M.
Proof.
elim: M.
- done.
- move=> /=. congruence.
- move=> /=. rewrite /upRen_pure_term_pure_term.
move=> > ?. under extRen_pure_term => ? do rewrite up_ren_id. by congruence.
Qed.
Lemma ren_pure_term_id' {ξ M} : (forall x, ξ x = x) -> ren_pure_term ξ M = M.
Proof. move=> ?. rewrite -[RHS]ren_pure_term_id. by apply: extRen_pure_term. Qed.
Fixpoint pure_var_bound (M: pure_term) :=
match M with
| pure_var x => 1 + x
| pure_app M N => 1 + pure_var_bound M + pure_var_bound N
| pure_abs M => 1 + pure_var_bound M
end.
Lemma pure_var_boundP M : allfv_pure_term (gt (pure_var_bound M)) M.
Proof.
elim: M.
- move=> /=. by lia.
- move=> ? IH1 ? IH2 /=. constructor; [move: IH1 | move: IH2]; apply: allfv_pure_term_impl; by lia.
- move=> ? /=. apply: allfv_pure_term_impl. case; first done. move=> /=. by lia.
Qed.
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
Require Import List Lia.
Import ListNotations.
Require Import Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped.
Import UnscopedNotations.
Require Import Undecidability.SystemF.Util.Facts Undecidability.SystemF.Util.poly_type_facts.
Require Import ssreflect ssrbool ssrfun.
Set Default Goal Selector "!".
(* evaluates predicate p on all free variables *)
Fixpoint allfv_pure_term (p: nat -> Prop) (M: pure_term) :=
match M with
| pure_var x => p x
| pure_app M N => allfv_pure_term p M /\ allfv_pure_term p N
| pure_abs M => allfv_pure_term (scons True p) M
end.
Lemma allfv_pure_term_impl {p1 p2: nat -> Prop} {M}:
(forall x, p1 x -> p2 x) -> allfv_pure_term p1 M -> allfv_pure_term p2 M.
Proof.
elim: M p1 p2.
- move=> >. by apply.
- by move=> ? IH1 ? IH2 > /= /copy [/IH1 {}IH1 /IH2 {}IH2] [/IH1 ? /IH2 ?].
- move=> > IH > H /=. apply: IH. by case.
Qed.
Lemma allfv_pure_term_ren_pure_term {p ξ M} :
allfv_pure_term p (ren_pure_term ξ M) <-> allfv_pure_term (ξ >> p) M.
Proof.
elim: M ξ p.
- done.
- move=> ? IH1 ? IH2 > /=. by rewrite IH1 IH2.
- move=> ? IH > /=. rewrite IH. constructor; apply: allfv_pure_term_impl; by case.
Qed.
Lemma allfv_pure_term_TrueI {p: nat -> Prop} {M} : (forall x, p x) -> allfv_pure_term p M.
Proof.
move=> Hp. elim: M.
- move=> > /=. by apply: Hp.
- by move=> ? + ? + /=.
- move=> ? /=. apply: allfv_pure_term_impl. case; first done.
move=> *. by apply: Hp.
Qed.
Lemma ren_pure_term_id {M} : ren_pure_term id M = M.
Proof.
elim: M.
- done.
- move=> /=. congruence.
- move=> /=. rewrite /upRen_pure_term_pure_term.
move=> > ?. under extRen_pure_term => ? do rewrite up_ren_id. by congruence.
Qed.
Lemma ren_pure_term_id' {ξ M} : (forall x, ξ x = x) -> ren_pure_term ξ M = M.
Proof. move=> ?. rewrite -[RHS]ren_pure_term_id. by apply: extRen_pure_term. Qed.
Fixpoint pure_var_bound (M: pure_term) :=
match M with
| pure_var x => 1 + x
| pure_app M N => 1 + pure_var_bound M + pure_var_bound N
| pure_abs M => 1 + pure_var_bound M
end.
Lemma pure_var_boundP M : allfv_pure_term (gt (pure_var_bound M)) M.
Proof.
elim: M.
- move=> /=. by lia.
- move=> ? IH1 ? IH2 /=. constructor; [move: IH1 | move: IH2]; apply: allfv_pure_term_impl; by lia.
- move=> ? /=. apply: allfv_pure_term_impl. case; first done. move=> /=. by lia.
Qed.