-(*
-let rec fresh_name G n \def
- match G with
- [ nil \Rightarrow n
- | (cons b H) \Rightarrow match (leb (fresh_name H n) (name b)) with
- [ true \Rightarrow (S (name b))
- | false \Rightarrow (fresh_name H n) ]].
-
-lemma freshname_Gn_geq_n : \forall G,n.((fresh_name G n) >= n).
-intro;elim G
- [simplify;unfold;constructor 1
- |simplify;cut ((leb (fresh_name l n) (name s)) = true \lor
- (leb (fresh_name l n) (name s) = false))
- [elim Hcut
- [lapply (leb_to_Prop (fresh_name l n) (name s));rewrite > H1 in Hletin;
- simplify in Hletin;rewrite > H1;simplify;lapply (H n);
- unfold in Hletin1;unfold;
- apply (trans_le ? ? ? Hletin1);
- apply (trans_le ? ? ? Hletin);constructor 2;constructor 1
- |rewrite > H1;simplify;apply H]
- |elim (leb (fresh_name l n) (name s)) [left;reflexivity|right;reflexivity]]]
-qed.
-
-lemma freshname_consGX_gt_X : \forall G,X,T,b,n.
- (fresh_name (cons ? (mk_bound b X T) G) n) > X.
-intros.unfold.unfold.simplify.cut ((leb (fresh_name G n) X) = true \lor
- (leb (fresh_name G n) X) = false)
- [elim Hcut
- [rewrite > H;simplify;constructor 1
- |rewrite > H;simplify;lapply (leb_to_Prop (fresh_name G n) X);
- rewrite > H in Hletin;simplify in Hletin;
- lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;assumption]
- |elim (leb (fresh_name G n) X) [left;reflexivity|right;reflexivity]]
-qed.
-
-lemma freshname_case : \forall G,X,T,b,n.
- (fresh_name ((mk_bound b X T) :: G) n) = (fresh_name G n) \lor
- (fresh_name ((mk_bound b X T) :: G) n) = (S X).
-intros.simplify.cut ((leb (fresh_name G n) X) = true \lor
- (leb (fresh_name G n) X) = false)
- [elim Hcut
- [rewrite > H;simplify;right;reflexivity
- |rewrite > H;simplify;left;reflexivity]
- |elim (leb (fresh_name G n) X)
- [left;reflexivity|right;reflexivity]]
-qed.
-
-lemma freshname_monotone_n : \forall G,m,n.(m \leq n) \to
- ((fresh_name G m) \leq (fresh_name G n)).
-intros.elim G
- [simplify;assumption
- |simplify;cut ((leb (fresh_name l m) (name s)) = true \lor
- (leb (fresh_name l m) (name s)) = false)
- [cut ((leb (fresh_name l n) (name s)) = true \lor
- (leb (fresh_name l n) (name s)) = false)
- [elim Hcut
- [rewrite > H2;simplify;elim Hcut1
- [rewrite > H3;simplify;constructor 1
- |rewrite > H3;simplify;
- lapply (leb_to_Prop (fresh_name l n) (name s));
- rewrite > H3 in Hletin;simplify in Hletin;
- lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;assumption]
- |rewrite > H2;simplify;elim Hcut1
- [rewrite > H3;simplify;
- lapply (leb_to_Prop (fresh_name l m) (name s));
- rewrite > H2 in Hletin;simplify in Hletin;
- lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;
- lapply (leb_to_Prop (fresh_name l n) (name s));
- rewrite > H3 in Hletin2;
- simplify in Hletin2;lapply (trans_le ? ? ? Hletin1 H1);
- lapply (trans_le ? ? ? Hletin3 Hletin2);
- absurd ((S (name s)) \leq (name s))
- [assumption|apply not_le_Sn_n]
- |rewrite > H3;simplify;assumption]]
- |elim (leb (fresh_name l n) (name s))
- [left;reflexivity|right;reflexivity]]
- |elim (leb (fresh_name l m) (name s)) [left;reflexivity|right;reflexivity]]]
-qed.
-
-lemma freshname_monotone_G : \forall G,X,T,b,n.
- (fresh_name G n) \leq (fresh_name ((mk_bound b X T) :: G) n).
-intros.simplify.cut ((leb (fresh_name G n) X) = true \lor
- (leb (fresh_name G n) X) = false)
- [elim Hcut
- [rewrite > H;simplify;lapply (leb_to_Prop (fresh_name G n) X);
- rewrite > H in Hletin;simplify in Hletin;constructor 2;assumption
- |rewrite > H;simplify;constructor 1]
- |elim (leb (fresh_name G n) X)
- [left;reflexivity|right;reflexivity]]
-qed.*)
-
-lemma subst_O_nat : \forall T,U.((subst_type_O T U) = (subst_type_nat T U O)).
-intros;elim T;simplify;reflexivity;
-qed.
-
-(* FIXME: these definitions shouldn't be part of the poplmark challenge
- - use destruct instead, when hopefully it will get fixed... *)
-
-definition head \def
- \lambda G:(list bound).match G with
- [ nil \Rightarrow (mk_bound false O Top)
- | (cons b H) \Rightarrow b].
-
-definition head_nat \def
- \lambda G:(list nat).match G with
- [ nil \Rightarrow O
- | (cons n H) \Rightarrow n].
-
-lemma inj_head : \forall h1,h2:bound.\forall t1,t2:Env.
- ((h1::t1) = (h2::t2)) \to (h1 = h2).
-intros.lapply (eq_f ? ? head ? ? H).simplify in Hletin.assumption.
-qed.
-
-lemma inj_head_nat : \forall h1,h2:nat.\forall t1,t2:(list nat).
- ((h1::t1) = (h2::t2)) \to (h1 = h2).
-intros.lapply (eq_f ? ? head_nat ? ? H).simplify in Hletin.assumption.
-qed.
-
-lemma inj_tail : \forall A.\forall h1,h2:A.\forall t1,t2:(list A).
- ((h1::t1) = (h2::t2)) \to (t1 = t2).
-intros.lapply (eq_f ? ? (tail ?) ? ? H).simplify in Hletin.assumption.
-qed.
-
-(* end of fixme *)
-
-(*** definitions and theorems about lists ***)
-
-inductive in_list (A : Set) : A \to (list A) \to Prop \def
- | in_Base : \forall x:A.\forall l:(list A).
- (in_list A x (x :: l))
- | in_Skip : \forall x,y:A.\forall l:(list A).
- (in_list A x l) \to (in_list A x (y :: l)).
-
-(* var binding is in env judgement *)
-definition var_bind_in_env : bound \to Env \to Prop \def
- \lambda b,G.(in_list bound b G).
-
-(* FIXME: use the map in library/list (when there will be one) *)
-definition map : \forall A,B,f.((list A) \to (list B)) \def
- \lambda A,B,f.let rec map (l : (list A)) : (list B) \def
- match l in list return \lambda l0:(list A).(list B) with
- [nil \Rightarrow (nil B)
- |(cons (a:A) (t:(list A))) \Rightarrow
- (cons B (f a) (map t))] in map.