(** Introduce.v Version 1.2 February 2011 *) (** runs under V8.3, tested with 8.3pl2 *) (** Celia Picard with contributions by Ralph Matthes, I.R.I.T., University of Toulouse and CNRS*) (** provides the definition of introduce and all associated tools and lemmas -- just to compare with extroduce *) Require Import Arith. Require Import Utf8. Require Import Setoid. Require Import Fin. Require Import Ilist. Require Import Tools. Require Import Extroduce. Set Implicit Arguments. (* introduces element t at place f in i *) Definition introduce: forall (T: Set)(t: T)(i: ilist T)(f: Fin (S (lgti i))), ilist T. Proof. intros T t [n i] f. simpl in f. apply (mkilist (n:=S n)). intro f'. elim (lt_eq_lt_dec (decode_Fin f') (decode_Fin f)) ; intros a. destruct a as [a|a]. exact (i (code_Fin1 (lt_le_trans _ _ _ a (lt_n_Sm_le _ _ (decode_Fin_inf_n f))))). exact t. exact (i (get_cons f' (lt_n_m_0 a))). Defined. Lemma introduce_lgti : forall (T: Set)(i: ilist T)(f: Fin (S (lgti i)))(t:T), lgti (introduce t i f) = S (lgti i). Proof. intros T [n i] f t. reflexivity. Defined. Lemma introduce_ok1': forall (T: Set)(i: ilist T)(f: Fin (S (lgti i)))(t:T) (f': Fin (lgti (introduce t i f))), decode_Fin f = decode_Fin f' -> fcti (introduce t i f) f' = t. Proof. intros T [n i] f t f' h. simpl in *|-*. elim (lt_eq_lt_dec (decode_Fin f') (decode_Fin f)) ; intros a; try destruct a as [a|a]; unfold sumor_rec, sumor_rect; try (apply False_rec ; rewrite h in a ; apply (lt_irrefl _ a)). reflexivity. Qed. Lemma introduce_ok2': forall (T: Set)(i: ilist T)(f: Fin (S (lgti i)))(t:T) (f': Fin (lgti (introduce t i f)))(h: decode_Fin f' < decode_Fin f), fcti (introduce t i f) f' = fcti i (code_Fin1 (lt_le_trans _ _ _ h (lt_n_Sm_le _ _ (decode_Fin_inf_n f)))). Proof. intros T [n i] f t f' h. simpl in *|-*. unfold sumor_rec, sumor_rect. elim (lt_eq_lt_dec (decode_Fin f') (decode_Fin f)) ; [intros [a|a]|intros a]. f_equal. destruct n as [|n]. revert h a ; rewrite (Fin_first_1 f'), (Fin_first_1 f) ; simpl ; intros h a. inversion h. apply code_Fin1_proofirr. apply False_rec, (lt_irrefl (decode_Fin f)). rewrite <- a at 1. assumption. apply False_rec, (lt_irrefl (decode_Fin f) (lt_trans _ _ _ a h)). Qed. Lemma inf_rewriteFins (n m r: nat)(i: Fin n)(h: n = m) : r < decode_Fin i -> r < decode_Fin (rewriteFins h i). Proof. intros h1. rewrite <- decode_Fin_match'. assumption. Qed. Lemma introduce_ok3': forall (T: Set)(i: ilist T)(f: Fin (S (lgti i)))(t:T) (f': Fin (lgti (introduce t i f)))(h: decode_Fin f < decode_Fin f'), fcti (introduce t i f) f' = fcti i (get_cons (rewriteFins (introduce_lgti _ _ _) f') (inf_rewriteFins f' (introduce_lgti _ _ _) (lt_n_m_0 h))). Proof. intros T [n i] f t f' h. simpl in *|-*. unfold sumor_rec, sumor_rect. elim (lt_eq_lt_dec (decode_Fin f') (decode_Fin f)) ; [intros a|intros a] ; [apply False_rec, (lt_irrefl (decode_Fin f)); destruct a as [a|a] | f_equal]. apply (lt_trans _ _ _ h a). rewrite <- a at 2. assumption. apply get_cons_proofirr. Qed. Lemma introduce_extroduce_id: forall (T: Set) (RelT : relation T) (EqT: Equivalence RelT) (i: ilist T) (f: Fin (lgti i)), ilist_rel RelT i (introduce (fcti i f) (extroduce i f) (rewriteFins (extroduce_lgti i f) f)). Proof. intros T RelT EqT i f. assert (h: lgti i = lgti (introduce (fcti i f) (extroduce i f) (rewriteFins (extroduce_lgti i f) f))). rewrite introduce_lgti. apply extroduce_lgti. apply (is_ilist_rel _ _ _ h). intro f'. destruct i as [n i]. simpl in f, f'. fold (mkilist i) in *|-*. change (fcti (mkilist i)) with i in *|-*. elim (lt_eq_lt_dec (decode_Fin (rewriteFins h f')) (decode_Fin (rewriteFins (extroduce_lgti (mkilist i) f) f))); try intros [b|b]; try intro b. rewrite (introduce_ok2' _ _ _ _ b ). rewrite extroduce_ok2'. apply (fRel EqT). treatFinPure. rewrite decode_code1_Id. rewrite <- (decode_Fin_match' _ (extroduce_lgti (mkilist i) f)) in b. assumption. rewrite introduce_ok1'. apply (fRel EqT), decode_Fin_unique. do 2 rewrite <- decode_Fin_match' in b. assumption. symmetry ; assumption. rewrite (introduce_ok3' _ _ _ _ b ). rewrite extroduce_ok3'. apply (fRel EqT). treatFinPure. apply le_S_n. rewrite <- decode_Fin_get_cons, <- decode_Fin_match'. rewrite <- (decode_Fin_match' _ (extroduce_lgti (mkilist i) f)) in b. apply gt_le_S, b. Qed. Lemma extroduce_introduce_id (T: Set) (RelT : relation T) (EqT: Equivalence RelT) (i: ilist T) (f: Fin (S (lgti i)))(t: T) : ilist_rel RelT i (extroduce (introduce t i f) (rewriteFins (sym_eq (introduce_lgti i f t)) f)). Proof. assert (h : lgti i = lgti (extroduce (introduce t i f) (rewriteFins (Logic.eq_sym (introduce_lgti i f t)) f))). apply eq_add_S. rewrite <- extroduce_lgti, introduce_lgti. reflexivity. apply (is_ilist_rel _ _ _ h). intros f'. elim (le_lt_dec (decode_Fin f) (decode_Fin f')) ; intros a. rewrite extroduce_ok3'. assert (h' : decode_Fin f < decode_Fin (rewriteFins (Logic.eq_sym (extroduce_lgti (introduce t i f) (rewriteFins (Logic.eq_sym (introduce_lgti i f t)) f))) (succ (rewriteFins h f')))). rewrite <- decode_Fin_match'. simpl. rewrite <- decode_Fin_match'. apply le_lt_n_Sm, a. rewrite (introduce_ok3' _ _ _ _ h'). apply (fRel EqT). treatFinPure. do 2 rewrite <- decode_Fin_match'. assumption. rewrite extroduce_ok2'. assert (h' : decode_Fin (rewriteFins (Logic.eq_sym (extroduce_lgti (introduce t i f) (rewriteFins (Logic.eq_sym (introduce_lgti i f t)) f))) (weakFin (rewriteFins h f'))) < decode_Fin f). rewrite <- decode_Fin_match', weakFin_ok, <- decode_Fin_match'. assumption. rewrite (introduce_ok2' _ _ _ _ h'). apply (fRel EqT). treatFinPure. do 2 rewrite <- decode_Fin_match'. assumption. Qed.