(* 2つの定義が等価であること *) Require Import problem1. Require Import problem2. Definition nth1 {A} := @problem1.nth A. Definition nth2 {A} := @problem2.nth A. Definition remove'_lst1 {A} := @problem1.remove'_lst A. Definition remove'_lst2 {A} := @problem2.remove'_lst A. Definition remove_lst1 {A} := @problem1.remove_lst A. Definition remove_lst2 {A} := @problem2.remove_lst A. (* problem1のremove'_lstとproblem2のremove'_lstが同値であること *) Lemma remove'_lst_compatible {A} : forall (l : list A) i (p : i < length l), remove'_lst2 l i (remove'_lst1 l i p). Proof. fix Ind 1. intros l i p. destruct l. exact (explosion _ (nleinil _ p)). destruct i. simpl. exact (is_remove_at_i_O _ _). simpl. apply is_remove_at_i_S. apply Ind. Qed. (* problem1のremove_lstとproblem2のremove_lstが同値であること *) Lemma remove_lst_compatible {A} : forall (ll : list (list A)) i (i_prf : i < length ll) j (j_prf : j < length (nth1 ll i i_prf)), remove_lst2 ll i j (remove_lst1 ll i i_prf j j_prf). Proof. fix Ind 1. intros ll i i_prf j j_prf. destruct ll as [| l ll']. exact (explosion _ (nleinil _ i_prf)). destruct i as [| i']. { simpl. apply remove_lst_O. exact (remove'_lst_compatible _ _ _). } { assert(i_prf' : i' < length ll'). { generalize i_prf. apply Coq.Arith.PeanoNat.Nat.succ_lt_mono. } assert(j_prf' : j < length (nth1 ll' i' i_prf')). { cut (nth1 ll' i' i_prf' = nth1 (cons l ll') (S i') i_prf). { intro relH. rewrite relH. assumption. } simpl. apply nth_proof_irrelevance. } cut (remove_lst1 (cons l ll') (S i') i_prf j j_prf = cons l (remove_lst1 ll' i' i_prf' j j_prf')). { intro relH. rewrite relH. apply remove_lst_S. apply Ind. } simpl. apply (fun_eq (fun x => cons l x)). apply remove_lst_proof_irrelevance; reflexivity. } Qed.