+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
-(* ||A|| E.Tassi, S.Zacchiroli *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU Lesser General Public License Version 2.1 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/library_auto/nat/permutation".
-
-include "nat/compare.ma".
-include "nat/sigma_and_pi.ma".
-
-definition injn: (nat \to nat) \to nat \to Prop \def
-\lambda f:nat \to nat.\lambda n:nat.\forall i,j:nat.
-i \le n \to j \le n \to f i = f j \to i = j.
-
-theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
-injn f (S n) \to injn f n.
-unfold injn.
-intros.
-apply H;auto.
-(*[ apply le_S.
- assumption
-| apply le_S.
- assumption
-| assumption
-]*)
-qed.
-
-theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
-injective nat nat f \to injn f n.
-unfold injective.
-unfold injn.
-intros.auto.
-(*apply H.
-assumption.*)
-qed.
-
-definition permut : (nat \to nat) \to nat \to Prop
-\def \lambda f:nat \to nat. \lambda m:nat.
-(\forall i:nat. i \le m \to f i \le m )\land injn f m.
-
-theorem permut_O_to_eq_O: \forall h:nat \to nat.
-permut h O \to (h O) = O.
-intros.
-unfold permut in H.
-elim H.
-apply sym_eq.auto.
-(*apply le_n_O_to_eq.
-apply H1.
-apply le_n.*)
-qed.
-
-theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat.
-permut f (S m) \to f (S m) = (S m) \to permut f m.
-unfold permut.
-intros.
-elim H.
-split
-[ intros.
- cut (f i < S m \lor f i = S m)
- [ elim Hcut
- [ auto
- (*apply le_S_S_to_le.
- assumption*)
- | apply False_ind.
- apply (not_le_Sn_n m).
- cut ((S m) = i)
- [ rewrite > Hcut1.
- assumption
- | apply H3
- [ apply le_n
- | auto
- (*apply le_S.
- assumption*)
- | auto
- (*rewrite > H5.
- assumption*)
- ]
- ]
- ]
- | apply le_to_or_lt_eq.
- auto
- (*apply H2.
- apply le_S.
- assumption*)
- ]
-| apply (injn_Sn_n f m H3)
-]
-qed.
-
-(* transpositions *)
-
-definition transpose : nat \to nat \to nat \to nat \def
-\lambda i,j,n:nat.
-match eqb n i with
- [ true \Rightarrow j
- | false \Rightarrow
- match eqb n j with
- [ true \Rightarrow i
- | false \Rightarrow n]].
-
-notation < "(❲i↹j❳)n"
- right associative with precedence 71
-for @{ 'transposition $i $j $n}.
-
-notation < "(❲i \atop j❳)n"
- right associative with precedence 71
-for @{ 'transposition $i $j $n}.
-
-interpretation "natural transposition" 'transposition i j n =
- (cic:/matita/library_auto/nat/permutation/transpose.con i j n).
-
-lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
-intros.
-unfold transpose.
-(*dopo circa 6 minuti, l'esecuzione di auto in questo punto non era ancora terminata*)
-rewrite > (eqb_n_n i).auto.
-(*simplify.
-reflexivity.*)
-qed.
-
-lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
-intros.
-unfold transpose.
-apply (eqb_elim j i)
-[ auto
- (*simplify.
- intro.
- assumption*)
-| rewrite > (eqb_n_n j).
- simplify.
- intros.
- reflexivity
-]
-qed.
-
-theorem transpose_i_i: \forall i,n:nat. (transpose i i n) = n.
-intros.
-unfold transpose.
-apply (eqb_elim n i)
-[ auto
- (*intro.
- simplify.
- apply sym_eq.
- assumption*)
-| intro.
- auto
- (*simplify.
- reflexivity*)
-]
-qed.
-
-theorem transpose_i_j_j_i: \forall i,j,n:nat.
-transpose i j n = transpose j i n.
-intros.
-unfold transpose.
-apply (eqb_elim n i)
-[ apply (eqb_elim n j)
- [ intros.
- (*l'esecuzione di auto in questo punto, dopo circa 300 secondi, non era ancora terminata*)
- simplify.auto
- (*rewrite < H.
- rewrite < H1.
- reflexivity*)
- | intros.
- auto
- (*simplify.
- reflexivity*)
- ]
-| apply (eqb_elim n j)
- [ intros.auto
- (*simplify.reflexivity *)
- | intros.auto
- (*simplify.reflexivity*)
- ]
-]
-qed.
-
-theorem transpose_transpose: \forall i,j,n:nat.
-(transpose i j (transpose i j n)) = n.
-intros.
-unfold transpose.
-unfold transpose.
-apply (eqb_elim n i)
-[ simplify.
- intro.
- apply (eqb_elim j i)
- [ simplify.
- intros.
- auto
- (*rewrite > H.
- rewrite > H1.
- reflexivity*)
- | rewrite > (eqb_n_n j).
- simplify.
- intros.
- auto
- (*apply sym_eq.
- assumption*)
- ]
-| apply (eqb_elim n j)
- [ simplify.
- rewrite > (eqb_n_n i).
- intros.
- auto
- (*simplify.
- apply sym_eq.
- assumption*)
- | simplify.
- intros.
- (*l'esecuzione di auto in questo punto, dopo piu' di 6 minuti non era ancora terminata*)
- rewrite > (not_eq_to_eqb_false n i H1).
- (*l'esecuzione di auto in questo punto, dopo piu' alcuni minuti non era ancora terminata*)
- rewrite > (not_eq_to_eqb_false n j H).auto
- (*simplify.
- reflexivity*)
- ]
-]
-qed.
-
-theorem injective_transpose : \forall i,j:nat.
-injective nat nat (transpose i j).
-unfold injective.
-intros.auto.
-(*rewrite < (transpose_transpose i j x).
-rewrite < (transpose_transpose i j y).
-apply eq_f.
-assumption.*)
-qed.
-
-variant inj_transpose: \forall i,j,n,m:nat.
-transpose i j n = transpose i j m \to n = m \def
-injective_transpose.
-
-theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to
-permut (transpose i j) n.
-unfold permut.
-intros.
-split
-[ unfold transpose.
- intros.
- elim (eqb i1 i)
- [ (*qui auto non chiude il goal*)
- simplify.
- assumption
- | elim (eqb i1 j)
- [ (*aui auto non chiude il goal*)
- simplify.
- assumption
- | (*aui auto non chiude il goal*)
- simplify.
- assumption
- ]
- ]
-| auto
- (*apply (injective_to_injn (transpose i j) n).
- apply injective_transpose*)
-]
-qed.
-
-theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat.
-permut f n \to permut g n \to permut (\lambda m.(f(g m))) n.
-unfold permut.
-intros.
-elim H.
-elim H1.
-split
-[ intros.
- simplify.
- auto
- (*apply H2.
- apply H4.
- assumption*)
-| simplify.
- intros.
- apply H5
- [ assumption
- | assumption
- | apply H3
- [ auto
- (*apply H4.
- assumption*)
- | auto
- (*apply H4.
- assumption*)
- | assumption
- ]
- ]
-]
-qed.
-
-theorem permut_transpose_l:
-\forall f:nat \to nat. \forall m,i,j:nat.
-i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
-intros.
-auto.
-(*apply (permut_fg (transpose i j) f m ? ?)
-[ apply permut_transpose;assumption
-| assumption
-]*)
-qed.
-
-theorem permut_transpose_r:
-\forall f:nat \to nat. \forall m,i,j:nat.
-i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
-intros.auto.
-(*apply (permut_fg f (transpose i j) m ? ?)
-[ assumption
-| apply permut_transpose;assumption
-]*)
-qed.
-
-theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
- \lnot i=k \to \lnot j=k \to
-transpose i j n = transpose i k (transpose k j (transpose i k n)).
-(* uffa: triplo unfold? *)
-intros.unfold transpose.
-unfold transpose.
-unfold transpose.
-apply (eqb_elim n i)
-[ intro.
- simplify.
- rewrite > (eqb_n_n k).
- simplify.
- rewrite > (not_eq_to_eqb_false j i H).
- rewrite > (not_eq_to_eqb_false j k H2).
- reflexivity
-| intro.
- apply (eqb_elim n j)
- [ intro.
- cut (\lnot n = k)
- [ cut (\lnot n = i)
- [ rewrite > (not_eq_to_eqb_false n k Hcut).
- simplify.
- rewrite > (not_eq_to_eqb_false n k Hcut).
- rewrite > (eq_to_eqb_true n j H4).
- simplify.
- rewrite > (not_eq_to_eqb_false k i)
- [ rewrite > (eqb_n_n k).
- auto
- (*simplify.
- reflexivity*)
- | unfold Not.
- intro.auto
- (*apply H1.
- apply sym_eq.
- assumption*)
- ]
- | assumption
- ]
- | unfold Not.
- intro.auto
- (*apply H2.
- apply (trans_eq ? ? n)
- [ apply sym_eq.
- assumption
- | assumption
- ]*)
- ]
- | intro.
- apply (eqb_elim n k)
- [ intro.
- simplify.
- rewrite > (not_eq_to_eqb_false i k H1).
- rewrite > (not_eq_to_eqb_false i j)
- [ simplify.
- rewrite > (eqb_n_n i).
- auto
- (*simplify.
- assumption*)
- | unfold Not.
- intro.auto
- (*apply H.
- apply sym_eq.
- assumption*)
- ]
- | intro.
- simplify.
- rewrite > (not_eq_to_eqb_false n k H5).
- rewrite > (not_eq_to_eqb_false n j H4).
- simplify.
- rewrite > (not_eq_to_eqb_false n i H3).
- rewrite > (not_eq_to_eqb_false n k H5).
- auto
- (*simplify.
- reflexivity*)
- ]
- ]
-]
-qed.
-
-theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
-\forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m)
-(f n)) m.
-unfold permut.
-intros.
-elim H.
-split
-[ intros.
- simplify.
- unfold transpose.
- apply (eqb_elim (f i) (f (S m)))
- [ intro.
- apply False_ind.
- cut (i = (S m))
- [ apply (not_le_Sn_n m).
- rewrite < Hcut.
- assumption
- | apply H2;auto
- (*[ apply le_S.
- assumption
- | apply le_n
- | assumption
- ]*)
- ]
- | intro.
- simplify.
- apply (eqb_elim (f i) (S m))
- [ intro.
- cut (f (S m) \lt (S m) \lor f (S m) = (S m))
- [ elim Hcut
- [ apply le_S_S_to_le.
- (*NB qui auto non chiude il goal*)
- assumption
- | apply False_ind.
- auto
- (*apply H4.
- rewrite > H6.
- assumption*)
- ]
- | auto
- (*apply le_to_or_lt_eq.
- apply H1.
- apply le_n*)
- ]
- | intro.simplify.
- cut (f i \lt (S m) \lor f i = (S m))
- [ elim Hcut
- [ auto
- (*apply le_S_S_to_le.
- assumption*)
- | apply False_ind.
- auto
- (*apply H5.
- assumption*)
- ]
- | apply le_to_or_lt_eq.
- auto
- (*apply H1.
- apply le_S.
- assumption*)
- ]
- ]
- ]
-| unfold injn.
- intros.
- apply H2;auto
- (*[ apply le_S.
- assumption
- | apply le_S.
- assumption
- | apply (inj_transpose (f (S m)) (S m)).
- apply H5
- ]*)
-]
-qed.
-
-(* bounded bijectivity *)
-
-definition bijn : (nat \to nat) \to nat \to Prop \def
-\lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
-ex nat (\lambda p. p \le n \land f p = m).
-
-theorem eq_to_bijn: \forall f,g:nat\to nat. \forall n:nat.
-(\forall i:nat. i \le n \to (f i) = (g i)) \to
-bijn f n \to bijn g n.
-intros 4.
-unfold bijn.
-intros.
-elim (H1 m)
-[ apply (ex_intro ? ? a).
- rewrite < (H a)
- [ assumption
- | elim H3.
- assumption
- ]
-| assumption
-]
-qed.
-
-theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
-bijn f (S n) \to f (S n) = (S n) \to bijn f n.
-unfold bijn.
-intros.
-elim (H m)
-[ elim H3.
- apply (ex_intro ? ? a).
- split
- [ cut (a < S n \lor a = S n)
- [ elim Hcut
- [ auto
- (*apply le_S_S_to_le.
- assumption*)
- | apply False_ind.
- apply (not_le_Sn_n n).
- rewrite < H1.
- rewrite < H6.
- rewrite > H5.
- assumption
- ]
- | auto
- (*apply le_to_or_lt_eq.
- assumption*)
- ]
- | assumption
- ]
-| auto
- (*apply le_S.
- assumption*)
-]
-qed.
-
-theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
-bijn f n \to f (S n) = (S n) \to bijn f (S n).
-unfold bijn.
-intros.
-cut (m < S n \lor m = S n)
-[ elim Hcut
- [ elim (H m)
- [ elim H4.
- apply (ex_intro ? ? a).
- auto
- (*split
- [ apply le_S.
- assumption
- | assumption
- ]*)
- | auto
- (*apply le_S_S_to_le.
- assumption*)
- ]
- | auto
- (*apply (ex_intro ? ? (S n)).
- split
- [ apply le_n
- | rewrite > H3.
- assumption
- ]*)
- ]
-| auto
- (*apply le_to_or_lt_eq.
- assumption*)
-]
-qed.
-
-theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
-bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
-unfold bijn.
-intros.
-simplify.
-elim (H m)
-[ elim H3.
- elim (H1 a)
- [ elim H6.
- auto
- (*apply (ex_intro ? ? a1).
- split
- [ assumption
- | rewrite > H8.
- assumption
- ]*)
- | assumption
- ]
-| assumption
-]
-qed.
-
-theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
-bijn (transpose i j) n.
-intros.
-unfold bijn.
-unfold transpose.
-intros.
-cut (m = i \lor \lnot m = i)
-[ elim Hcut
- [ apply (ex_intro ? ? j).
- split
- [ assumption
- | apply (eqb_elim j i)
- [ intro.
- (*dopo circa 360 secondi l'esecuzione di auto in questo punto non era ancora terminata*)
- simplify.
- auto
- (*rewrite > H3.
- rewrite > H4.
- reflexivity*)
- | rewrite > (eqb_n_n j).
- simplify.
- intros.
- auto
- (*apply sym_eq.
- assumption*)
- ]
- ]
- | cut (m = j \lor \lnot m = j)
- [ elim Hcut1
- [ apply (ex_intro ? ? i).
- split
- [ assumption
- | (*dopo circa 5 minuti, l'esecuzione di auto in questo punto non era ancora terminata*)
- rewrite > (eqb_n_n i).
- auto
- (*simplify.
- apply sym_eq.
- assumption*)
- ]
- | apply (ex_intro ? ? m).
- split
- [ assumption
- | rewrite > (not_eq_to_eqb_false m i)
- [ (*dopo circa 5 minuti, l'esecuzione di auto in questo punto non era ancora terminata*)
- rewrite > (not_eq_to_eqb_false m j)
- [ auto
- (*simplify.
- reflexivity*)
- | assumption
- ]
- | assumption
- ]
- ]
- ]
- | apply (decidable_eq_nat m j)
- ]
- ]
-| apply (decidable_eq_nat m i)
-]
-qed.
-
-theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
-bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
-intros.auto.
-(*apply (bijn_fg f ?)
-[ assumption
-| apply (bijn_transpose n i j)
- [ assumption
- | assumption
- ]
-]*)
-qed.
-
-theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
-bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
-intros.
-auto.
-(*apply (bijn_fg ? f)
-[ apply (bijn_transpose n i j)
- [ assumption
- | assumption
- ]
-| assumption
-]*)
-qed.
-
-theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
-permut f n \to bijn f n.
-intro.
-elim n
-[ unfold bijn.
- intros.
- apply (ex_intro ? ? m).
- split
- [ assumption
- | apply (le_n_O_elim m ? (\lambda p. f p = p))
- [ assumption
- | unfold permut in H.
- elim H.
- apply sym_eq.
- auto
- (*apply le_n_O_to_eq.
- apply H2.
- apply le_n*)
- ]
- ]
-| apply (eq_to_bijn (\lambda p.
- (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f)
- [ intros.
- apply transpose_transpose
- | apply (bijn_fg (transpose (f (S n1)) (S n1)))
- [ apply bijn_transpose
- [ unfold permut in H1.
- elim H1.auto
- (*apply H2.
- apply le_n*)
- | apply le_n
- ]
- | apply bijn_n_Sn
- [ apply H.
- auto
- (*apply permut_S_to_permut_transpose.
- assumption*)
- | auto
- (*unfold transpose.
- rewrite > (eqb_n_n (f (S n1))).
- simplify.
- reflexivity*)
- ]
- ]
- ]
-]
-qed.
-
-let rec invert_permut n f m \def
- match eqb m (f n) with
- [true \Rightarrow n
- |false \Rightarrow
- match n with
- [O \Rightarrow O
- |(S p) \Rightarrow invert_permut p f m]].
-
-theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
-m \le n \to injn f n\to invert_permut n f (f m) = m.
-intros 4.
-elim H
-[ apply (nat_case1 m)
- [ intro.
- simplify.
- (*l'applicazione di auto in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
- rewrite > (eqb_n_n (f O)).
- auto
- (*simplify.
- reflexivity*)
- | intros.simplify.
- (*l'applicazione di auto in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
- rewrite > (eqb_n_n (f (S m1))).
- auto
- (*simplify.
- reflexivity*)
- ]
-| simplify.
- rewrite > (not_eq_to_eqb_false (f m) (f (S n1)))
- [ (*l'applicazione di auto in questo punto, dopo parecchi secondi, non aveva ancora prodotto un risultato*)
- simplify.
- auto
- (*apply H2.
- apply injn_Sn_n.
- assumption*)
- | unfold Not.
- intro.
- absurd (m = S n1)
- [ apply H3;auto
- (*[ apply le_S.
- assumption
- | apply le_n
- | assumption
- ]*)
- | unfold Not.
- intro.
- apply (not_le_Sn_n n1).
- rewrite < H5.
- assumption
- ]
- ]
-]
-qed.
-
-theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
-permut f n \to injn (invert_permut n f) n.
-intros.
-unfold injn.
-intros.
-cut (bijn f n)
-[ unfold bijn in Hcut.
- generalize in match (Hcut i H1).
- intro.
- generalize in match (Hcut j H2).
- intro.
- elim H4.
- elim H6.
- elim H5.
- elim H9.
- rewrite < H8.
- rewrite < H11.
- apply eq_f.
- rewrite < (invert_permut_f f n a)
- [ rewrite < (invert_permut_f f n a1)
- [ rewrite > H8.
- rewrite > H11.
- assumption
- | assumption
- | unfold permut in H.elim H.
- assumption
- ]
- | assumption
- | unfold permut in H.
- elim H.
- assumption
- ]
-| auto
- (*apply permut_to_bijn.
- assumption*)
-]
-qed.
-
-theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
-permut f n \to permut (invert_permut n f) n.
-intros.
-unfold permut.
-split
-[ intros.
- simplify.
- elim n
- [ simplify.
- elim (eqb i (f O));auto
- (*[ simplify.
- apply le_n
- | simplify.
- apply le_n
- ]*)
- | simplify.
- elim (eqb i (f (S n1)))
- [ auto
- (*simplify.
- apply le_n*)
- | simplify.
- auto
- (*apply le_S.
- assumption*)
- ]
- ]
-| auto
- (*apply injective_invert_permut.
- assumption.*)
-]
-qed.
-
-theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
-m \le n \to permut f n\to f (invert_permut n f m) = m.
-intros.
-apply (injective_invert_permut f n H1)
-[ unfold permut in H1.
- elim H1.
- apply H2.
- cut (permut (invert_permut n f) n)
- [ unfold permut in Hcut.
- elim Hcut.auto
- (*apply H4.
- assumption*)
- | apply permut_invert_permut.
- (*NB qui auto non chiude il goal*)
- assumption
- ]
-| assumption
-| apply invert_permut_f
- [ cut (permut (invert_permut n f) n)
- [ unfold permut in Hcut.
- elim Hcut.
- auto
- (*apply H2.
- assumption*)
- | auto
- (*apply permut_invert_permut.
- assumption*)
- ]
- | unfold permut in H1.
- elim H1.
- assumption
- ]
-]
-qed.
-
-theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
-permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
-intros.
-unfold permut in H.
-elim H.
-cut (invert_permut n h n < n \lor invert_permut n h n = n)
-[ elim Hcut
- [ rewrite < (f_invert_permut h n n) in \vdash (? ? ? %)
- [ apply eq_f.
- rewrite < (f_invert_permut h n n) in \vdash (? ? % ?)
- [ auto
- (*apply H1.
- assumption*)
- | apply le_n
- | (*qui auto NON chiude il goal*)
- assumption
- ]
- | apply le_n
- | (*qui auto NON chiude il goal*)
- assumption
- ]
- | rewrite < H4 in \vdash (? ? % ?).
- apply (f_invert_permut h)
- [ apply le_n
- | (*qui auto NON chiude il goal*)
- assumption
- ]
- ]
-| apply le_to_or_lt_eq.
- cut (permut (invert_permut n h) n)
- [ unfold permut in Hcut.
- elim Hcut.
- auto
- (*apply H4.
- apply le_n*)
- | apply permut_invert_permut.
- (*NB aui auto non chiude il goal*)
- assumption
- ]
-]
-qed.
-
-theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
-k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
-\forall j. k \le j \to j \le n \to k \le h j.
-intros.
-unfold permut in H1.
-elim H1.
-cut (h j < k \lor \not(h j < k))
-[ elim Hcut
- [ absurd (k \le j)
- [ assumption
- | apply lt_to_not_le.
- cut (h j = j)
- [ rewrite < Hcut1.
- assumption
- | apply H6;auto
- (*[ apply H5.
- assumption
- | assumption
- | apply H2.
- assumption
- ]*)
- ]
- ]
- | auto
- (*apply not_lt_to_le.
- assumption*)
- ]
-| apply (decidable_lt (h j) k)
-]
-qed.
-
-(* applications *)
-
-let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
- match k with
- [ O \Rightarrow g i
- | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
-
-theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
-\forall f:nat \to nat \to nat. \forall n,i:nat.
-(\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to
-map_iter_i n g1 f i = map_iter_i n g2 f i.
-intros 5.
-elim n
-[ simplify.
- auto
- (*apply H
- [ apply le_n
- | apply le_n
- ]*)
-| simplify.
- apply eq_f2
- [ auto
- (*apply H1
- [ simplify.
- apply le_S.
- apply le_plus_n
- | simplify.
- apply le_n
- ]*)
- | apply H.
- intros.
- apply H1;auto
- (*[ assumption
- | simplify.
- apply le_S.
- assumption
- ]*)
- ]
-]
-qed.
-
-(* map_iter examples *)
-
-theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat.
-map_iter_i n g plus m = sigma n g m.
-intros.
-elim n
-[ auto
- (*simplify.
- reflexivity*)
-| simplify.
- auto
- (*apply eq_f.
- assumption*)
-]
-qed.
-
-theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat.
-map_iter_i n g times m = pi n g m.
-intros.
-elim n
-[ auto
- (*simplify.
- reflexivity*)
-| simplify.
- auto
- (*apply eq_f.
- assumption*)
-]
-qed.
-
-theorem eq_map_iter_i_fact: \forall n:nat.
-map_iter_i n (\lambda m.m) times (S O) = (S n)!.
-intros.
-elim n
-[ auto
- (*simplify.
- reflexivity*)
-| change with
- (((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!).
- rewrite < plus_n_Sm.
- rewrite < plus_n_O.
- apply eq_f.
- (*NB: qui auto non chiude il goal!!!*)
- assumption
-]
-qed.
-
-
-theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
-map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n.
-intros.
-apply (nat_case1 k)
-[ intros.
- simplify.
- fold simplify (transpose n (S n) (S n)).
- auto
- (*rewrite > transpose_i_j_i.
- rewrite > transpose_i_j_j.
- apply H1*)
-| intros.
- change with
- (f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
- f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
- (f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
- (map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
- rewrite > transpose_i_j_i.
- rewrite > transpose_i_j_j.
- rewrite < H.
- rewrite < H.
- rewrite < (H1 (g (S m + n))).
- apply eq_f.
- apply eq_map_iter_i.
- intros.
- simplify.
- unfold transpose.
- rewrite > (not_eq_to_eqb_false m1 (S m+n))
- [ rewrite > (not_eq_to_eqb_false m1 (S (S m)+n))
- [ auto
- (*simplify.
- reflexivity*)
- | apply (lt_to_not_eq m1 (S ((S m)+n))).
- auto
- (*unfold lt.
- apply le_S_S.
- change with (m1 \leq S (m+n)).
- apply le_S.
- assumption*)
- ]
- | apply (lt_to_not_eq m1 (S m+n)).
- simplify.auto
- (*unfold lt.
- apply le_S_S.
- assumption*)
- ]
-]
-qed.
-
-theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
-map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
-intros 6.
-elim k
-[ cut (i=n)
- [ rewrite > Hcut.
- (*qui auto non chiude il goal*)
- apply (eq_map_iter_i_transpose_l f H H1 g n O)
- | apply antisymmetric_le
- [ assumption
- | assumption
- ]
- ]
-| cut (i < S n1 + n \lor i = S n1 + n)
- [ elim Hcut
- [ change with
- (f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
- f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n)).
- apply eq_f2
- [ unfold transpose.
- rewrite > (not_eq_to_eqb_false (S (S n1)+n) i)
- [ rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i))
- [ auto
- (*simplify.
- reflexivity*)
- | simplify.
- unfold Not.
- intro.
- apply (lt_to_not_eq i (S n1+n))
- [ assumption
- | auto
- (*apply inj_S.
- apply sym_eq.
- assumption*)
- ]
- ]
- | simplify.
- unfold Not.
- intro.
- apply (lt_to_not_eq i (S (S n1+n)))
- [ auto
- (*simplify.
- unfold lt.
- apply le_S_S.
- assumption*)
- | auto
- (*apply sym_eq.
- assumption*)
- ]
- ]
- | apply H2;auto
- (*[ assumption
- | apply le_S_S_to_le.
- assumption
- ]*)
- ]
- | rewrite > H5.
- (*qui auto non chiude il goal*)
- apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
- ]
- | auto
- (*apply le_to_or_lt_eq.
- assumption*)
- ]
-]
-qed.
-
-theorem eq_map_iter_i_transpose:
-\forall f:nat\to nat \to nat.
-associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat.
-\forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
-map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
-intros 6.
-apply (nat_elim1 o).
-intro.
-apply (nat_case m ?)
-[ intros.
- apply (eq_map_iter_i_transpose_i_Si ? H H1);auto
- (*[ exact H3
- | apply le_S_S_to_le.
- assumption
- ]*)
-| intros.
- apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n))
- [ apply H2
- [ auto
- (*unfold lt.
- apply le_n*)
- | assumption
- | apply (trans_le ? (S(S (m1+i))))
- [ auto
- (*apply le_S.
- apply le_n*)
- | (*qui auto non chiude il goal, chiuso invece da assumption*)
- assumption
- ]
- ]
- | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
- (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n))
- [ (*qui auto dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
- apply (H2 O ? ? (S(m1+i)))
- [ auto
- (*unfold lt.
- apply le_S_S.
- apply le_O_n*)
- | auto
- (*apply (trans_le ? i)
- [ assumption
- | change with (i \le (S m1)+i).
- apply le_plus_n
- ]*)
- | (*qui auto non chiude il goal*)
- exact H4
- ]
- | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
- (transpose i (S(m1 + i))
- (transpose (S(m1 + i)) (S(S(m1 + i)))
- (transpose i (S(m1 + i)) m)))) f n))
- [ (*qui auto dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
- apply (H2 m1)
- [ auto
- (*unfold lt.
- apply le_n*)
- | assumption
- | apply (trans_le ? (S(S (m1+i))))
- [ auto
- (*apply le_S.
- apply le_n*)
- | (*qui auto NON CHIUDE il goal*)
- assumption
- ]
- ]
- | apply eq_map_iter_i.
- intros.
- apply eq_f.
- apply sym_eq.
- apply eq_transpose
- [ unfold Not.
- intro.
- apply (not_le_Sn_n i).
- rewrite < H7 in \vdash (? ? %).
- auto
- (*apply le_S_S.
- apply le_S.
- apply le_plus_n*)
- | unfold Not.
- intro.
- apply (not_le_Sn_n i).
- rewrite > H7 in \vdash (? ? %).
- auto
- (*apply le_S_S.
- apply le_plus_n*)
- | unfold Not.
- intro.
- auto
- (*apply (not_eq_n_Sn (S m1+i)).
- apply sym_eq.
- assumption*)
- ]
- ]
- ]
- ]
-]
-qed.
-
-theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall n,k,i,j:nat.
-\forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to
-map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
-intros.
-simplify in H3.
-cut ((S i) < j \lor (S i) = j)
-[ elim Hcut
- [ cut (j = S ((j - (S i)) + i))
- [ rewrite > Hcut1.
- apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i)
- [ assumption
- | rewrite < Hcut1.
- assumption
- ]
- | rewrite > plus_n_Sm.
- auto
- (*apply plus_minus_m_m.
- apply lt_to_le.
- assumption*)
- ]
- | rewrite < H5.
- apply (eq_map_iter_i_transpose_i_Si f H H1 g)
- [ auto
- (*simplify.
- assumption*)
- | apply le_S_S_to_le.
- auto
- (*apply (trans_le ? j)
- [ assumption
- | assumption
- ]*)
- ]
- ]
-| auto
- (*apply le_to_or_lt_eq.
- assumption*)
-]
-qed.
-
-theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall n,k,i,j:nat.
-\forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to
-map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
-intros.
-apply (nat_compare_elim i j)
-[ intro.
- (*qui auto non chiude il goal*)
- apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5)
-| intro.
- rewrite > H6.
- apply eq_map_iter_i.
- intros.
- auto
- (*rewrite > (transpose_i_i j).
- reflexivity*)
-| intro.
- apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n))
- [ apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3)
- | apply eq_map_iter_i.
- intros.
- auto
- (*apply eq_f.
- apply transpose_i_j_j_i*)
- ]
-]
-qed.
-
-theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
-permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
-map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
-intros 4.
-elim k
-[ simplify.
- rewrite > (permut_n_to_eq_n h)
- [ reflexivity
- | (*qui auto non chiude il goal*)
- assumption
- | (*qui auto non chiude il goal*)
- assumption
- ]
-| apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1))
- [ unfold permut in H3.
- elim H3.
- apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g)
- [ apply (permut_n_to_le h n1 (S n+n1))
- [ apply le_plus_n
- | (*qui auto non chiude il goal*)
- assumption
- | (*qui auto non chiude il goal*)
- assumption
- | apply le_plus_n
- | apply le_n
- ]
- | auto
- (*apply H5.
- apply le_n*)
- | apply le_plus_n
- | apply le_n
- ]
- | apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
- (g(transpose (h (S n+n1)) (S n+n1)
- (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1))
- [ simplify.
- fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
- apply eq_f2
- [ auto
- (*apply eq_f.
- rewrite > transpose_i_j_j.
- rewrite > transpose_i_j_i.
- rewrite > transpose_i_j_j.
- reflexivity.*)
- | apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
- [ apply permut_S_to_permut_transpose.
- (*qui auto non chiude il goal*)
- assumption
- | intros.
- unfold transpose.
- rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1)))
- [ rewrite > (not_eq_to_eqb_false (h m) (S n+n1))
- [ simplify.
- auto
- (*apply H4.
- assumption*)
- | rewrite > H4
- [ auto
- (*apply lt_to_not_eq.
- apply (trans_lt ? n1)
- [ assumption
- | simplify.
- unfold lt.
- apply le_S_S.
- apply le_plus_n
- ]*)
- | assumption
- ]
- ]
- | unfold permut in H3.
- elim H3.
- simplify.
- unfold Not.
- intro.
- apply (lt_to_not_eq m (S n+n1))
- [ auto
- (*apply (trans_lt ? n1)
- [ assumption
- | simplify.
- unfold lt.
- apply le_S_S.
- apply le_plus_n
- ]*)
- | unfold injn in H7.
- apply (H7 m (S n+n1))
- [ auto
- (*apply (trans_le ? n1)
- [ apply lt_to_le.
- assumption
- | apply le_plus_n
- ]*)
- | apply le_n
- | assumption
- ]
- ]
- ]
- ]
- ]
- | apply eq_map_iter_i.
- intros.
- auto
- (*rewrite > transpose_transpose.
- reflexivity*)
- ]
- ]
-]
-qed.
\ No newline at end of file
projects / helm.git / blobdiff