-
Notifications
You must be signed in to change notification settings - Fork 0
/
IlistPerm.v
1958 lines (1826 loc) · 78.1 KB
/
IlistPerm.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(** Celia Picard with contributions by Ralph Matthes,
I.R.I.T., University of Toulouse and CNRS*)
(** provides the definition of various relations of permutation
on ilist with associated tools and lemmas *)
Require Import Fin.
Require Import Ilist.
Require Import Setoid.
Require Import Extroduce.
Require Import Utf8.
Require Import Basics.
Require Import Morphisms.
Require Import Tools.
Set Implicit Arguments.
(* this section corresponds to the developments around ilist_perm_occ in the paper (section 2.1) *)
Section Ilist_Perm_occ.
Fixpoint count_occn (T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(t: T)(n: nat)
(i: ilistn T n){struct n} : nat :=
match n as m return (ilistn T m -> nat) with
0 => fun _: ilistn T 0 => 0
| S m => fun i0: ilistn T (S m) =>
if (R_dec t (i0 (first m))) then
S (count_occn RelT R_dec t (fun f => i0 (succ f)))
else (count_occn RelT R_dec t (fun f => i0 (succ f)))
end i.
(* Counts number of occurrences of t in i *)
(* called nb_occ in the paper - Definition 7 *)
Definition count_occ(T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(t: T)(i: ilist T) : nat :=
let (n, i') := i in count_occn RelT R_dec t i'.
Add Parametric Morphism (T: Set)(RelT: relation T)(RelTEq: Equivalence RelT)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(t: T):
(count_occ RelT R_dec t)
with signature (ilist_rel RelT ==> @eq nat)
as count_occM1.
Proof.
intros [n1 i1] [n2 i2] [h H].
cbn in h, H.
assert (h' := h) ; revert i2 h H ; rewrite <- h' ; intros i2 h H ; clear h' n2.
fold (mkilist i1); fold (mkilist i2).
assert (e1: forall f, f = rewriteFins h f).
{ intro f.
apply decode_Fin_unique, decode_Fin_match'. }
assert (H': forall f, RelT (i1 f) (i2 f)).
{ intro f ; rewrite (e1 f) at 2 ; apply H. }
clear h H e1.
cbn.
induction n1 as [|n IH].
{ reflexivity. }
cbn.
destruct RelTEq as [Rrefl Rsym Rtrans].
elim (R_dec t (i1 (first n))) ; intros a ;
elim (R_dec t (i2 (first n))) ; intros c ;
rewrite (IH _ (fun f : Fin n => i2 (succ f)));
try reflexivity ;
try (intro f ; apply H') ;
try assert (b := Rtrans _ _ _ a (H' (first n))) ;
try assert (b := Rtrans _ _ _ c (Rsym _ _ (H' (first n)))) ;
contradiction b.
Qed.
(* Indicates whether an ilist is a permutation of another using decidability *)
(* Called ilist_perm_occ in the paper - Definition 8 *)
Inductive IlistPerm (T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(i1 i2: ilist T): Prop :=
is_IlistPerm: (forall t: T,
count_occ RelT R_dec t i1 =
count_occ RelT R_dec t i2) ->
IlistPerm RelT R_dec i1 i2.
Lemma count_occn_in (T: Set)(RelT: relation T)(Req: Equivalence RelT)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(n: nat)(l : ilistn T n)(i: Fin n) :
exists m, count_occn RelT R_dec (l i) l = S m.
Proof.
induction i.
- cbn.
elim (R_dec (l (first k)) (l (first k))) ; intros a.
+ exists (count_occn RelT R_dec (l (first k)) (fun f : Fin k => l (succ f))).
reflexivity.
+ unfold not in a.
contradiction a.
reflexivity.
- cbn.
elim (R_dec (l (succ i)) (l (first k))) ; intros a.
+ exists (count_occn RelT R_dec (l (succ i)) (fun f : Fin k => l (succ f))).
reflexivity.
+ destruct (IHi (fun f : Fin k => l (succ f))) as [m H].
exists m.
apply H.
Qed.
Lemma count_occn_not_exist (T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(n: nat)(l : ilistn T n)(t: T):
not (exists i: Fin n, RelT t (l i)) -> count_occn RelT R_dec t l = 0.
Proof.
intros H.
induction n as [|n IH].
{ reflexivity. }
cbn.
elim (R_dec t (l (first n))) ; intros a.
- destruct H.
exists (first n) ; assumption.
- apply IH.
intros [f H'].
destruct H.
exists (succ f) ; assumption.
Qed.
Lemma count_occn_exist (T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(n: nat)(l : ilistn T n)(t: T)(m: nat):
count_occn RelT R_dec t l = S m -> exists i: Fin n, RelT t (l i).
Proof.
intro H.
induction n as [|n IH].
{ inversion H. }
cbn in H.
revert H.
elim (R_dec t (l (first n))) ; cbn ; intros a H.
- exists (first n) ; assumption.
- destruct (IH (fun x => l (succ x)) H) as [f H'].
exists (succ f) ; assumption.
Qed.
Lemma IlistPerm_refl: forall (T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(i1: ilist T),
IlistPerm RelT R_dec i1 i1.
Proof.
intros T RelT R_dec i1.
apply is_IlistPerm.
reflexivity.
Qed.
Lemma IlistPerm_sym: forall (T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(i1 i2: ilist T),
IlistPerm RelT R_dec i1 i2 -> IlistPerm RelT R_dec i2 i1.
Proof.
intros T RelT Req i1 i2 [H].
apply is_IlistPerm.
intro t.
apply (sym_eq (H t)).
Qed.
Lemma IlistPerm_trans: forall (T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(i1 i2 i3: ilist T),
IlistPerm RelT R_dec i1 i2 -> IlistPerm RelT R_dec i2 i3 ->
IlistPerm RelT R_dec i1 i3.
Proof.
intros T RelT R_dec i1 i2 i3 [H1] [H2].
apply is_IlistPerm.
intro t.
apply (trans_eq (H1 t) (H2 t)).
Qed.
Add Parametric Relation(T: Set)(RelT: relation T)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)}):
(ilist T) (@IlistPerm T RelT R_dec)
reflexivity proved by (@IlistPerm_refl T RelT R_dec)
symmetry proved by (@IlistPerm_sym T RelT R_dec)
transitivity proved by (@IlistPerm_trans T RelT R_dec)
as IlistPermRel.
Add Parametric Morphism (T: Set)(RelT: relation T)(REq: Equivalence RelT)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(i: ilist T):
(fun x => count_occ RelT R_dec x i)
with signature (RelT ==> @eq nat)
as count_occM2.
Proof.
intros t1 t2 H.
destruct i as [n i].
cbn.
induction n as [|n IH].
{ reflexivity. }
cbn.
destruct REq as [Rrefl Rsym Rtrans].
elim (R_dec t1 (i (first n))) ; intros a ;
elim (R_dec t2 (i (first n))) ; intros b ;
try (rewrite IH ; reflexivity);
try assert (c := Rtrans _ _ _ (Rsym _ _ H) a) ;
try assert (c := Rtrans _ _ _ H b) ;
contradiction c.
Qed.
Lemma ilist_rel_finer_IlistPerm:
forall (T: Set)(RelT: relation T) (REq : Equivalence RelT)
(R_dec: forall x y, {RelT x y}+{not (RelT x y)})(i1 i2: ilist T),
ilist_rel RelT i1 i2 -> IlistPerm RelT R_dec i1 i2.
Proof.
intros T RelT [Rrefl Rsym Rtrans] R_dec [n i1] [n2 i2] [h H].
apply is_IlistPerm.
intros t.
cbn in *|-*.
assert (h' := h) ; revert i1 i2 h H ; rewrite <- h' ; intros i1 i2 h H ; clear h' n2.
assert (H1 : forall f, RelT (i1 f) (i2 f)).
{ intro f.
rewrite (decode_Fin_unique _ _ (decode_Fin_match' f h)) at 2.
apply (H f). }
clear H h.
induction n as [|n IH].
{ reflexivity. }
cbn.
elim (R_dec t (i1 (first n))) ; elim (R_dec t (i2 (first n))) ; intros a b.
- f_equal ; apply IH.
intro f ; apply (H1 (succ f)).
- contradiction (Rtrans _ _ _ b (H1 (first n))).
- contradiction (Rtrans _ _ _ a (Rsym _ _ (H1 (first n)))).
- apply IH.
intro f ; apply (H1 (succ f)).
Qed.
End Ilist_Perm_occ.
Section IlistPerm_ind.
(* In the paper, iperm *)
Inductive IlistPerm3 (T: Set)(RelT: relation T)(i1 i2: ilist T): Prop :=
IlistPerm3_nil: lgti i1 = lgti i2 -> lgti i1 = 0 -> IlistPerm3 RelT i1 i2
| IlistPerm3_cons: forall f1 f2, RelT (fcti i1 f1) (fcti i2 f2) ->
IlistPerm3 RelT (extroduce i1 f1) (extroduce i2 f2) ->
IlistPerm3 RelT i1 i2.
(* In the paper, iperm' *)
Inductive IlistPerm4 (T: Set)(RelT: relation T): ilist T-> ilist T-> Prop :=
is_IlistPerm4: forall (i1 i2: ilist T), lgti i1 = lgti i2 ->
(forall f1, exists f2, RelT (fcti i1 f1) (fcti i2 f2) /\
IlistPerm4 RelT (extroduce i1 f1) (extroduce i2 f2)) ->
IlistPerm4 RelT i1 i2.
Scheme IlistPerm4_ind_rich := Induction for IlistPerm4 Sort Prop.
Lemma IlistPerm4_ind_better : forall (T : Set)(RelT : relation T)(P : ilist T -> ilist T -> Prop),
(forall i1 i2 : ilist T, lgti i1 = lgti i2 ->
(forall f1 : Fin (lgti i1), exists f2 : Fin (lgti i2),
RelT (fcti i1 f1) (fcti i2 f2) /\ IlistPerm4 RelT (extroduce i1 f1) (extroduce i2 f2) /\
P (extroduce i1 f1) (extroduce i2 f2)) -> P i1 i2)
-> (forall i i0 : ilist T, IlistPerm4 RelT i i0 -> P i i0).
Proof.
intros T RelT P H.
refine (fix Hr (i00 i0: ilist T)(h: IlistPerm4 RelT i00 i0){struct h} : P i00 i0 :=
match h with is_IlistPerm4 i1 i2 h1 h2 => _ end).
clear i00 i0 h.
apply H.
{ assumption. }
intro f1.
destruct (h2 f1) as [f2 [h3 h4]].
exists f2.
split ; try split ; try assumption.
apply (Hr _ _ h4).
Qed.
Inductive IlistPerm5 (T: Set)(RelT: relation T): ilist T -> ilist T -> Prop :=
is_IlistPerm5: forall (i1 i2: ilist T), lgti i1 = lgti i2 ->
(forall f2, exists f1, RelT (fcti i1 f1) (fcti i2 f2) /\
IlistPerm5 RelT (extroduce i1 f1) (extroduce i2 f2)) ->
IlistPerm5 RelT i1 i2.
Lemma IlistPerm5_ind_better : forall (T : Set)(RelT : relation T)(P : ilist T → ilist T → Prop),
(forall i1 i2 : ilist T, lgti i1 = lgti i2 ->
(forall f2 : Fin (lgti i2), exists f1 : Fin (lgti i1),
RelT (fcti i1 f1) (fcti i2 f2) /\ IlistPerm5 RelT (extroduce i1 f1) (extroduce i2 f2) /\
P (extroduce i1 f1) (extroduce i2 f2)) -> P i1 i2)
-> (forall i i0 : ilist T, IlistPerm5 RelT i i0 -> P i i0).
Proof.
intros T RelT P H.
refine (fix Hr (i00 i0: ilist T)(h: IlistPerm5 RelT i00 i0){struct h} : P i00 i0 :=
match h with is_IlistPerm5 i1 i2 h1 h2 => _ end).
clear i00 i0 h.
apply H.
{ assumption. }
intro f2.
destruct (h2 f2) as [f1 [h3 h4]].
exists f1.
split ; try split ; try assumption.
apply (Hr _ _ h4).
Qed.
Lemma IlistPerm3_lgti: forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm3 RelT i1 i2 -> lgti i1 = lgti i2.
Proof.
intros T RelT i1 i2 H.
induction H as [i1 i2 h1 h2 | i1 i2 f1 f2 h1 h2 IH].
{ assumption. }
apply eq_S in IH.
do 2 rewrite <- extroduce_lgti in IH.
assumption.
Qed.
(* D2 => D1 *)
Lemma IlistPerm4_IlistPerm3_eq : forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm4 RelT i1 i2 -> IlistPerm3 RelT i1 i2.
Proof.
intros T RelT i1 i2 h.
induction h as [i1 i2 h1 h2] using IlistPerm4_ind_better.
destruct i1 as [n1 i1]; destruct i2 as [n2 i2].
simpl lgti in h1, h2 ; simpl fcti in h2.
fold (mkilist i1) in *|-*.
fold (mkilist i2) in *|-*.
destruct n1 as [|n1].
- apply IlistPerm3_nil.
+ assumption.
+ reflexivity.
- destruct (h2 (first n1)) as [f2 [h3 [h4 h5]]] ; clear h2.
clear h4.
apply (IlistPerm3_cons _ _ (first _: Fin (lgti (mkilist _)))
(f2: Fin (lgti (mkilist _)))) ; assumption.
Qed.
Lemma IlistPerm5_IlistPerm3_eq : forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm5 RelT i1 i2 -> IlistPerm3 RelT i1 i2.
Proof.
intros T RelT i1 i2 h.
induction h as [i1 i2 h1 h2] using IlistPerm5_ind_better.
destruct i1 as [n1 i1]; destruct i2 as [n2 i2].
simpl lgti in h1, h2 ; simpl fcti in h2.
fold (mkilist i1) in *|-*.
fold (mkilist i2) in *|-*.
destruct n2 as [|n2].
- apply IlistPerm3_nil ; assumption.
- destruct (h2 (first n2)) as [f1 [h3 [h4 h5]]] ; clear h2.
clear h4.
apply (IlistPerm3_cons _ _ (f1 : Fin (lgti (mkilist _)))
(first _: Fin (lgti (mkilist _)))) ; assumption.
Qed.
Lemma IlistPerm4_refl_refl: forall (T: Set)(RelT: relation T)(Rrefl: Reflexive RelT)(i: ilist T),
IlistPerm4 RelT i i.
Proof.
intros T RelT Rrefl [n i].
induction n as [|n IH] ;
apply (is_IlistPerm4 _ _ (refl_equal _)) ;
simpl lgti ; simpl fcti ;
intro f ; exists f.
- inversion f.
- split.
+ reflexivity.
+ set (e := extroduce (existT (fun n0 : nat => ilistn T n0) (S n) i) f).
assert (h:= extroduce_lgti_S _ _ : n = lgti e).
destruct e as [n' e].
cbn in h ; revert e ; rewrite <- h ; intro e ; apply IH.
Qed.
Lemma IlistPerm4_refl: forall (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(i: ilist T),
IlistPerm4 RelT i i.
Proof.
intros T RelT [Rrefl _ _] [n i].
induction n as [|n IH] ;
apply (is_IlistPerm4 _ _ (refl_equal _)) ;
simpl lgti ; simpl fcti ;
intro f ; exists f.
- inversion f.
- split.
+ apply Rrefl.
+ set (e := extroduce (existT (fun n0 : nat => ilistn T n0) (S n) i) f).
assert (h: lgti e = n).
{ apply eq_add_S.
unfold e.
rewrite <- extroduce_lgti.
reflexivity. }
destruct e as [n' e].
cbn in h ; revert e ; rewrite h ; intro e ; apply IH.
Qed.
(* Deduced from IlistPerm4_refl *)
Lemma IlistPerm3_refl_refl: forall (T: Set)(RelT: relation T)(Rrefl: Reflexive RelT)(i: ilist T),
IlistPerm3 RelT i i.
Proof.
intros T RelT Rrefl i.
apply IlistPerm4_IlistPerm3_eq.
apply (IlistPerm4_refl_refl Rrefl).
Qed.
(* Deduced from IlistPerm4_refl *)
Lemma IlistPerm3_refl: forall (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(i: ilist T),
IlistPerm3 RelT i i.
Proof.
intros T RelT EqT i.
apply IlistPerm4_IlistPerm3_eq.
apply (IlistPerm4_refl EqT).
Qed.
Lemma IlistPerm3nil: forall (T: Set)(RelT: relation T)(i1 i2: ilistn T 0),
IlistPerm3 RelT (mkilist (n:=0) i1) (mkilist (n:=0) i2).
Proof.
intros T RelT i1 i2.
apply IlistPerm3_nil ; reflexivity.
Qed.
Lemma IlistPerm4nil: forall (T: Set)(RelT: relation T)(i1 i2: ilistn T 0),
IlistPerm4 RelT (mkilist (n:=0) i1) (mkilist (n:=0) i2).
Proof.
intros T RelT i1 i2.
apply is_IlistPerm4.
- reflexivity.
- intro f1 ; inversion f1.
Qed.
Lemma IlistPerm4nil_gen: forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
lgti i1 = lgti i2 -> lgti i1 = 0 ->
IlistPerm4 RelT i1 i2.
Proof.
intros T RelT i1 i2 Hyp1 Hyp2.
apply is_IlistPerm4.
- exact Hyp1.
- intro f1.
apply False_rec.
rewrite Hyp2 in f1.
inversion f1.
Qed.
Lemma IlistPerm4_lgti: forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm4 RelT i1 i2 -> lgti i1 = lgti i2.
Proof.
intros T RelT _ _ [i1 i2 e1 _] ; assumption.
Qed.
Lemma IlistPerm3_flip: forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm3 RelT i1 i2 -> IlistPerm3 (flip RelT) i2 i1.
Proof.
intros T RelT i1 i2 ; intros h ;
induction h as [i1 i2 e1 e2 | i1 i2 f1 f2 h1 _ IH].
- apply (IlistPerm3_nil _ _ _ (sym_eq e1) (trans_eq (sym_eq e1) e2)).
- apply (IlistPerm3_cons _ _ f2 f1) ; assumption.
Qed.
Lemma IlistPerm3_flip': forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm3 (flip RelT) i1 i2 -> IlistPerm3 RelT i2 i1.
Proof.
intros T RelT i1 i2 ; intros h ;
induction h as [i1 i2 e1 e2 | i1 i2 f1 f2 h1 h2 IH].
- apply (IlistPerm3_nil _ _ _ (sym_eq e1) (trans_eq (sym_eq e1) e2)).
- apply (IlistPerm3_cons _ _ f2 f1); assumption.
Qed.
(* using IlistPerm3_flip *)
Lemma IlistPerm3_sym: forall (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(i1 i2: ilist T),
IlistPerm3 RelT i1 i2 -> IlistPerm3 RelT i2 i1.
Proof.
intros T RelT [_ Rsym _] i1 i2 h.
assert (h1 := IlistPerm3_flip h) ; clear h.
induction h1 as [i2 i1 e1 e2 | i2 i1 f2 f1 h1 _ IH].
- apply (IlistPerm3_nil _ _ _ e1 e2).
- apply (IlistPerm3_cons _ _ f2 f1).
+ apply (Rsym _ _ h1).
+ assumption.
Qed.
Lemma IlistPerm3_sym_sym: forall (T: Set)(RelT: relation T)(Rsym: Symmetric RelT)(i1 i2: ilist T),
IlistPerm3 RelT i1 i2 -> IlistPerm3 RelT i2 i1.
Proof.
intros T RelT Rsym i1 i2 h.
assert (h1 := IlistPerm3_flip h) ; clear h.
induction h1 as [i1 i2 e1 e2 | i1 i2 f1 f2 h1 h2 IH].
- apply (IlistPerm3_nil _ _ _ e1 e2).
- apply (IlistPerm3_cons _ _ f1 f2).
+ apply (Rsym _ _ h1).
+ assumption.
Qed.
Definition TransitiveAt (T: Type)(R: relation T)(t1: T): Prop :=
forall (t2 t3: T), R t1 t2 -> R t2 t3 -> R t1 t3.
Lemma IlistPerm4_trans_refined:
forall (T: Set)(RelT: relation T)(i1: ilist T),
(forall f1: Fin (lgti i1), TransitiveAt RelT (fcti i1 f1)) ->
TransitiveAt (IlistPerm4 RelT) i1.
Proof.
intros T RelT i1 Hyp i2 i3 h1 h2.
revert i1 h1 Hyp.
induction h2 as [i2 i3 e2 h2] using IlistPerm4_ind_better.
intros i1 h1 Hyp.
destruct h1 as [i1 i2 e1 h1].
apply is_IlistPerm4.
- apply (trans_eq e1 e2).
- intro f1.
destruct (h1 f1) as [f2 [h11 h12]] ; clear h1.
destruct (h2 f2) as [f3 [h21 [h22 h23]]] ; clear h2.
exists f3.
split.
+ apply (Hyp _ _ _ h11 h21).
+ apply (h23 _ h12).
intro f0.
destruct (extroduce_ok_cor i1 f1 f0).
rewrite H.
apply Hyp.
Qed.
(* obviously, the following lemma is just a special case *)
Lemma IlistPerm4_trans:
forall (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(i1 i2 i3: ilist T),
IlistPerm4 RelT i1 i2 -> IlistPerm4 RelT i2 i3 -> IlistPerm4 RelT i1 i3.
Proof.
intros T RelT [_ _ Rtrans] i1.
change (TransitiveAt (IlistPerm4 RelT) i1).
apply IlistPerm4_trans_refined.
red.
intros.
transitivity t2; assumption.
Qed.
Lemma IlistPerm4_trans_trans:
forall (T: Set)(RelT: relation T)(Rtrans: Transitive RelT)(i1 i2 i3: ilist T),
IlistPerm4 RelT i1 i2 -> IlistPerm4 RelT i2 i3 -> IlistPerm4 RelT i1 i3.
Proof.
intros T RelT Rtrans i1.
change (TransitiveAt (IlistPerm4 RelT) i1).
apply IlistPerm4_trans_refined.
intros f1 t2 t3 H1 H2.
transitivity t2; assumption.
Qed.
Lemma IlistPerm4_flip_IlistPerm5 : forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm4 RelT i1 i2 -> IlistPerm5 (flip RelT) i2 i1.
Proof.
intros T RelT i1 i2 H.
induction H as [i1 i2 h1 h2] using IlistPerm4_ind_better.
apply (is_IlistPerm5 _ _ (sym_eq h1)).
intro f1.
destruct (h2 f1) as [f2 [h3 [_ h4]]].
exists f2.
split ; assumption.
Qed.
Lemma IlistPerm4_sym_IlistPerm5 : forall (T: Set)(RelT: relation T)(Rsym: symmetric _ RelT)
(i1 i2: ilist T), IlistPerm4 RelT i1 i2 -> IlistPerm5 RelT i2 i1.
Proof.
intros T RelT Rsym i1 i2 h.
assert (h1:= IlistPerm4_flip_IlistPerm5 h) ; clear h.
induction h1 as [i1 i2 h1 h2] using IlistPerm5_ind_better.
apply (is_IlistPerm5 _ _ h1).
intro f2.
destruct (h2 f2) as [f1 [h3 [_ h4]]].
exists f1.
split.
- apply (Rsym _ _ h3).
- assumption.
Qed.
Lemma IlistPerm5_flip_IlistPerm4 : forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm5 RelT i1 i2 -> IlistPerm4 (flip RelT) i2 i1.
Proof.
intros T RelT i1 i2 H.
induction H as [i1 i2 h1 h2] using IlistPerm5_ind_better.
apply (is_IlistPerm4 _ _ (sym_eq h1)).
intro f1.
destruct (h2 f1) as [f2 [h3 [_ h4]]].
exists f2.
split ; assumption.
Qed.
Lemma IlistPerm5_sym_IlistPerm4 : forall (T: Set)(RelT: relation T)(Rsym: symmetric _ RelT)
(i1 i2: ilist T), IlistPerm5 RelT i1 i2 -> IlistPerm4 RelT i2 i1.
Proof.
intros T RelT Rsym i1 i2 h.
assert (h1:= IlistPerm5_flip_IlistPerm4 h) ; clear h.
induction h1 as [i1 i2 h1 h2] using IlistPerm4_ind_better.
apply (is_IlistPerm4 _ _ h1).
intro f2.
destruct (h2 f2) as [f1 [h3 [_ h4]]].
exists f1.
split.
- apply (Rsym _ _ h3).
- assumption.
Qed.
(* deduced from IlistPerm4_refl *)
Lemma IlistPerm5_refl: forall (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(i: ilist T),
IlistPerm5 RelT i i.
Proof.
intros T RelT EqT i.
apply IlistPerm4_sym_IlistPerm5.
- destruct EqT as [_ Rsym _] ; assumption.
- apply (IlistPerm4_refl EqT).
Qed.
(* Proof by induction on IlistPerm4 *)
Lemma IlistPerm4_ilist_rel: forall (T: Set)(RelT: relation T)(EqT: Equivalence RelT)
(i1 i1' i2 : ilist T), ilist_rel RelT i1 i1' -> IlistPerm4 RelT i1 i2 ->
IlistPerm4 RelT i1' i2.
Proof.
intros T RelT EqT i1 i1' i2 h1 h2.
apply (ilist_rel_sym _) in h1.
revert i1' h1.
induction h2 as [i1 i2 e2 h2] using IlistPerm4_ind_better ; intros i1' h1.
destruct h1 as [e1 h1'].
apply (is_IlistPerm4 _ _ (trans_eq e1 e2)).
intro f1.
destruct (h2 (rewriteFins e1 f1)) as [f3 [h3 [h4 IH]]].
exists f3.
split.
- destruct EqT as [_ _ Rtrans].
apply (Rtrans _ _ _ (h1' f1) h3).
- apply IH.
assert (h : lgti (extroduce i1' f1) = lgti (extroduce i1 (rewriteFins e1 f1))).
{ evalLgtiExtro.
assumption. }
apply (is_ilist_rel _ _ _ h).
intro f.
elim (le_lt_dec (decode_Fin f1) (decode_Fin f)) ; intros a.
+ rewrite extroduce_ok3' ; try assumption.
rewrite extroduce_ok3' by (treatFin a).
assert (h5: rewriteFins (sym_eq (extroduce_lgti i1 (rewriteFins e1 f1))) (succ (rewriteFins h f)) =
rewriteFins e1 (rewriteFins (sym_eq (extroduce_lgti i1' f1)) (succ f))).
{ treatFinPure. }
rewrite h5.
apply h1'.
+ rewrite extroduce_ok2' ; try assumption.
rewrite extroduce_ok2' by (treatFin a).
assert (h5: rewriteFins (sym_eq (extroduce_lgti i1 (rewriteFins e1 f1)))
(weakFin (rewriteFins h f)) = rewriteFins e1
(rewriteFins (sym_eq (extroduce_lgti i1' f1)) (weakFin f))).
* treatFinPure.
* rewrite h5.
apply h1'.
Qed.
(* Proof with induction on IlistPerm3 *)
Lemma IlistPerm3_ilist_rel: forall (T: Set)(RelT: relation T)(EqT: Equivalence RelT)
(i1 i1' i2 : ilist T), ilist_rel RelT i1 i1' -> IlistPerm3 RelT i1 i2 ->
IlistPerm3 RelT i1' i2.
Proof.
intros T RelT EqT i1 i1' i2 h1 h2.
revert i1' h1 ; induction h2 as [i1 i2 e2 e3 | i1 i2 f1 f2 e2 h2 IH] ; intros i1' [e1 h1].
- apply (IlistPerm3_nil _ _ _ (trans_eq (sym_eq e1) e2) (trans_eq (sym_eq e1) e3)).
- apply (IlistPerm3_cons _ _ (rewriteFins e1 f1) f2).
+ destruct EqT as [_ Rsym Rtrans].
apply (Rtrans _ _ _ (Rsym _ _ (h1 f1)) e2).
+ apply IH.
assert (h3: lgti (extroduce i1 f1) = lgti (extroduce i1' (rewriteFins e1 f1))).
{ evalLgtiExtro.
assumption. }
apply (is_ilist_rel _ _ _ h3).
intro f.
elim (le_lt_dec (decode_Fin f1) (decode_Fin f)) ; intros a.
(* continue as for IlistPerm4_ilist_rel (only variable names have changed) *)
* rewrite extroduce_ok3' ; try assumption.
rewrite extroduce_ok3' by (treatFin a).
assert (h4: rewriteFins (sym_eq (extroduce_lgti i1' (rewriteFins e1 f1))) (succ (rewriteFins h3 f)) =
rewriteFins e1 (rewriteFins (sym_eq (extroduce_lgti i1 f1)) (succ f))).
{ treatFinPure. }
rewrite h4.
apply h1.
* rewrite extroduce_ok2' ; try assumption.
rewrite extroduce_ok2' by (treatFin a).
assert (h5: rewriteFins (sym_eq (extroduce_lgti i1' (rewriteFins e1 f1)))
(weakFin (rewriteFins h3 f)) = rewriteFins e1
(rewriteFins (sym_eq (extroduce_lgti i1 f1)) (weakFin f))).
{ treatFinPure. }
rewrite h5.
apply h1.
Qed.
Lemma IlistPerm3_ilist_rel_eq: forall (T: Set)(RelT: relation T)(l1 l1' l2 : ilist T)
(h: ilist_rel (@eq T) l1 l1'), IlistPerm3 RelT l1 l2 -> IlistPerm3 RelT l1' l2.
Proof.
intros T RelT l1 l1' l2 h1 h2.
revert l1' h1 ; induction h2 as [l1 l2 e2 e3 | l1 l2 i1 i2 e2 h2 IH] ; intros l1' h1 ;
inversion h1 as [e1 h1'].
- apply (IlistPerm3_nil _ _ _ (trans_eq (sym_eq e1) e2) (trans_eq (sym_eq e1) e3)).
- apply (IlistPerm3_cons _ _ (rewriteFins e1 i1) i2).
+ rewrite <- (h1' i1).
assumption.
+ apply IH.
apply extroduce_ilist_rel_bis.
assumption.
Qed.
(* just a dual proof for the changes in the second argument *)
Lemma IlistPerm3_ilist_rel_eq_snd: forall (T: Set)(RelT: relation T)(l1 l2 l2' : ilist T)
(h: ilist_rel (@eq T) l2 l2'), IlistPerm3 RelT l1 l2 -> IlistPerm3 RelT l1 l2'.
Proof.
intros T RelT l1 l1' l2 h1 h2.
revert l2 h1 ; induction h2 as [l1 l2 e2 e3 | l1 l2 i1 i2 e2 h2 IH] ; intros l1' h1 ;
inversion h1 as [e1 h1'].
apply (IlistPerm3_nil _ _ _ (trans_eq e2 e1) e3).
apply (IlistPerm3_cons _ _ i1 (rewriteFins e1 i2)).
rewrite <- (h1' i2).
assumption.
apply IH.
apply extroduce_ilist_rel_bis.
assumption.
Qed.
Add Parametric Morphism (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(l: ilist T) :
(fun x => IlistPerm3 RelT x l)
with signature (ilist_rel RelT ==> impl) as IlistPerm3M1_Eq.
Proof.
intros l2 l2' H2 H3.
apply (IlistPerm3_ilist_rel EqT H2 H3).
Qed.
Add Parametric Morphism (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(l: ilist T) :
(IlistPerm3 RelT l)
with signature (ilist_rel RelT ==> impl) as IlistPerm3M2_Eq.
Proof.
intros l1 l1' H2 H3.
apply (IlistPerm3_sym EqT).
apply (IlistPerm3_sym EqT) in H3.
apply (IlistPerm3_ilist_rel EqT H2 H3).
Qed.
Add Parametric Morphism (T: Set)(RelT: relation T)(EqT: Equivalence RelT):
(IlistPerm3 RelT)
with signature (ilist_rel RelT ==> ilist_rel RelT ==> impl) as IlistPerm3M_Eq.
Proof.
intros l1 l1' H1 l2 l2' H2 H3.
apply (IlistPerm3M2_Eq EqT H2).
apply (IlistPerm3M1_Eq EqT H1).
assumption.
Qed.
Lemma ilist_rel_finer_IlistPerm3: forall (T: Set)(RelT: relation T)
(i1 i2 : ilist T), ilist_rel RelT i1 i2 -> IlistPerm3 RelT i1 i2.
Proof.
intros T RelT [n l1] [n2 l2] H.
inversion H as [h2 _].
cbn in h2.
revert l2 H ; rewrite <- h2 ; intros l2 H ; clear n2 h2.
induction n as [|n IH].
- destruct H as [h H] ; cbn in *|-*.
apply IlistPerm3_nil ; reflexivity.
- assert (i := first n).
apply (IlistPerm3_cons _ _ (i: Fin (lgti (existT (fun n0 : nat => ilistn T n0) (S n) l1)))
(i: Fin (lgti (existT (fun n0 : nat => ilistn T n0) (S n) l2)))).
+ destruct H as [h H].
assert (H1: forall i, RelT (l1 i) (l2 i)).
{ intro i'.
assert (h' : i' = rewriteFins h i').
unfold rewriteFins; apply decode_Fin_unique, decode_Fin_match.
rewrite h' at 2 ; apply (H i'). }
clear h H.
apply H1.
+ assert (H1 := extroduce_ilist_rel i H).
revert H1 ; unfold mkilist.
set (l1' := extroduce (existT (fun n0 : nat => ilistn T n0) (S n) l1) i).
set (l2' := extroduce (existT (fun n0 : nat => ilistn T n0) (S n) l2) i).
intro H1.
assert (h: lgti l1' = n).
{ unfold l1' ; apply eq_add_S.
rewrite <- extroduce_lgti.
reflexivity. }
destruct l1' as [n' l1'] ; destruct l2' as [n2 l2'].
inversion H1 as [h1 _].
cbn in *|-*.
revert l1' l2' H1.
rewrite <- h1, h.
apply IH.
Qed.
Lemma ilist_rel_finer_IlistPerm4: forall (T: Set)(RelT: relation T)
(l1 l2 : ilist T), ilist_rel RelT l1 l2 -> IlistPerm4 RelT l1 l2.
Proof.
intros T RelT [n l1] [n2 l2] h.
inversion h as [h2 _].
cbn in h2.
revert l2 h ; rewrite <- h2 ; intros l2 h ; clear n2 h2.
fold (mkilist l1) (mkilist l2).
induction n as [|n IH].
{ apply IlistPerm4nil. }
apply (is_IlistPerm4 _ _ (refl_equal _ : lgti (mkilist l1) = lgti (mkilist l2))).
intro i.
inversion h as [e h'].
simpl lgti in *|-* ; simpl fcti in *|-*.
exists i.
split.
- rewrite (decode_Fin_unique _ _ (decode_Fin_match' i e)) at 2.
apply h'.
- assert (hex := extroduce_ilist_rel i h).
revert hex.
set (l1' := extroduce (mkilist l1) i) ; set (l2' := extroduce (mkilist l2) i) ;
assert (h1 := extroduce_lgti_S l1 i :n = lgti l1') ; assert (h2 := extroduce_lgti_S l2 i :n = lgti l2').
destruct l1' as [n1 l1'] ; destruct l2' as [n2 l2'].
cbn in h1, h2.
revert l1' l2' ; rewrite <- h1, <- h2 ; clear n1 n2 h1 h2.
apply IH.
Qed.
Lemma IlistPerm3_imap (T U: Set)(RelT: relation T)(RelU: relation U)
(f: T -> U)(fM: Proper (RelT ==> RelU) f) (l1 l2: ilist T):
IlistPerm3 RelT l1 l2 -> IlistPerm3 RelU (imap f l1) (imap f l2).
Proof.
intro H ; induction H as [[n1 l1] [n2 l2] e1 e2 | l1 l2 i1 i2 h2 H IH].
{ apply IlistPerm3_nil ; assumption. }
apply (IlistPerm3_cons _ _ (i1 : Fin (lgti(imap f l1))) (i2: Fin (lgti (imap f l2)))).
- cbn.
apply fM, h2.
- apply (IlistPerm3_ilist_rel_eq (ilist_rel_sym _ (extroduce_imap f l1 i1))).
apply (IlistPerm3_ilist_rel_eq_snd (ilist_rel_sym _ (extroduce_imap f l2 i2))).
apply IH.
Qed.
Lemma IlistPerm3_imap_bis (A B: Set)(Rel: relation B)(f1 f2: A -> B)(l1 l2: ilist A):
IlistPerm3 (fun a1 a2 => Rel (f1 a1) (f2 a2)) l1 l2 -> IlistPerm3 Rel (imap f1 l1) (imap f2 l2).
Proof.
intro Hyp.
induction Hyp as [l1 l2 Hyp1 Hyp2 | l1 l2 i1 i2 H1 _ IH].
{ apply IlistPerm3_nil ; assumption. }
apply (IlistPerm3_cons _ _ (i1 : Fin (lgti (imap f1 l1))) (i2 : Fin (lgti (imap f2 l2)))).
- assumption.
- assert (H7 := extroduce_imap f1 l1 i1).
apply ilist_rel_sym in H7 ; try apply eq_equivalence.
apply (IlistPerm3_ilist_rel_eq H7).
clear H7.
assert (H7 := extroduce_imap f2 l2 i2).
apply ilist_rel_sym in H7 ; try apply eq_equivalence.
apply (IlistPerm3_ilist_rel_eq_snd H7).
assumption.
Qed.
Lemma IlistPerm3_imap_back (A B: Set)(Rel: relation B)
(f1 f2: A -> B)(l1 l2: ilist A): IlistPerm3 Rel (imap f1 l1) (imap f2 l2) ->
IlistPerm3 (fun a1 a2 => Rel (f1 a1) (f2 a2)) l1 l2.
Proof.
remember (lgti l1) as n.
revert l1 l2 Heqn ; induction n as [|n IH] ; intros l1 l2 H H1.
- apply IlistPerm3_nil.
+ apply (IlistPerm3_lgti H1).
+ symmetry ; assumption.
- inversion_clear H1 as [H2 H3 | i1 i2 H2 H3].
+ cbn in H3 ; rewrite <- H in H3.
inversion H3.
+ cbn in i1, i2, H2.
apply (IlistPerm3_cons _ _ i1 i2).
* assumption.
* apply IH.
-- evalLgtiExtro.
apply H.
-- assert (H4 := extroduce_imap f1 l1 i1).
assert (H5 := extroduce_imap f2 l2 i2).
apply (IlistPerm3_ilist_rel_eq H4), (IlistPerm3_ilist_rel_eq_snd H5), H3.
Qed.
Lemma IlistPerm3_exists_rec: forall (T: Set)(RelT: relation T)
(i1 i2: ilist T), IlistPerm3 RelT i1 i2 -> forall f1, exists f2, RelT (fcti i1 f1) (fcti i2 f2) /\
IlistPerm3 RelT (extroduce i1 f1) (extroduce i2 f2).
Proof.
intros T RelT l1 l2 H.
induction H as [l1 l2 _ e2 | l1 l2 i1 i2 h2 H IH].
- (* empty list *)
intros i1.
apply False_rec.
rewrite e2 in i1.
inversion i1.
- (* non-empty list *)
assert (h1:= eq_S _ _ (IlistPerm3_lgti H)).
do 2 rewrite <- extroduce_lgti in h1.
destruct l1 as [n l1] ; destruct l2 as [n2 l2];
cbn in i1, i2, h1, h2 ;
fold (mkilist l1) in *|-*;
fold (mkilist l2) in *|-*.
revert l2 i2 h2 H IH ; rewrite <- h1 ; intros l2 i2 h2 H IH ; clear n2 h1.
change (forall i1', exists i2', RelT (l1 i1') (l2 i2') /\
IlistPerm3 RelT (extroduce (mkilist l1) i1') (extroduce (mkilist l2) i2')).
intros i1'.
(* is there something to do renaming? *)
elim (eq_nat_dec (decode_Fin i1) (decode_Fin i1')) ; intros a.
+ (* f1 = f1' *)
rewrite <- (decode_Fin_unique _ _ a).
exists i2.
split; assumption.
+ (* f1 <> f1' *)
destruct n as [|n].
* (* exclude zero case *)
inversion i1.
* (* main case *)
set (i1'new := index_in_extroduce i1 i1' a).
destruct (IH (rewriteFins (extroduce_lgti_S _ i1) i1'new)) as [i2IH [IH1 IH2]].
set (i2IH' := rewriteFins (sym_eq (extroduce_lgti_S _ i2)) i2IH).
set (i2' := extroduce_Fin i2 i2IH').
exists i2'.
split.
-- assert (h3: l1 i1' = fcti (extroduce (mkilist l1) i1) (rewriteFins (extroduce_lgti_S l1 i1) i1'new)) by
apply index_in_extroduce_ok_cor.
assert (h4: l2 i2' = fcti (extroduce (mkilist l2) i2) i2IH).
{ unfold i2', i2IH'.
rewrite extroduce_Fin_ok_cor.
f_equal.
treatFinPure. }
rewrite h3, h4.
assumption.
-- set (i1new := index_in_extroduce i1' i1 (not_eq_sym a)).
assert (a2: decode_Fin i2' <> decode_Fin i2).
{ unfold i2'.
intro Hyp.
apply decode_Fin_unique in Hyp.
apply (extroduce_Fin_not_fex _ Hyp). }
set (i2new := index_in_extroduce i2' i2 a2).
apply (IlistPerm3_cons _ _ (rewriteFins (extroduce_lgti_S l1 i1') i1new)
(rewriteFins (extroduce_lgti_S l2 i2') i2new)).
++ unfold i1new.
rewrite <- index_in_extroduce_ok_cor.
unfold i2new.
rewrite <- index_in_extroduce_ok_cor.
exact h2.
++ assert (H1:= extroduce_interchange_eq l1 i1' i1 (not_eq_sym a) a).
fold i1new i1'new in H1.
assert (H2:= extroduce_interchange_eq l2 i2' i2 a2 (not_eq_sym a2)).
fold i2new in H2.
apply ilist_rel_sym in H1 ; apply ilist_rel_sym in H2 ; try apply eq_equivalence.
apply (IlistPerm3_ilist_rel_eq H1), (IlistPerm3_ilist_rel_eq_snd H2).
assert (H3 : i2IH = rewriteFins (extroduce_lgti_S l2 i2) (index_in_extroduce i2 i2' (not_eq_sym a2))).
{ unfold i2', i2IH'.
rewrite index_in_from_extroduce.
apply decode_Fin_unique.
do 2 rewrite <- decode_Fin_match'.
reflexivity. }
rewrite <- H3.
assumption.
Qed.
(* from the Coq tutorial at POPL'08 *)
Tactic Notation "remember" constr(c) "as" ident(x) "in" "|-" :=
let x := fresh x in
let H := fresh "Heq" x in
(set (x := c); assert (H : x = c) by reflexivity; clearbody x).
Lemma IlistPerm3_IlistPerm4_eq: forall (T: Set)(RelT: relation T)(i1 i2: ilist T),
IlistPerm3 RelT i1 i2 -> IlistPerm4 RelT i1 i2.
Proof.
intros T RelT l1 l2 H.
remember (lgti l1) as n in |-.
revert l1 l2 H Heqn ; induction n as [|n IH]; intros l1 l2 H Heqn ; cbn in *|-*.
- apply IlistPerm4nil_gen.
+ apply (IlistPerm3_lgti H).
+ symmetry; assumption.
- apply is_IlistPerm4.
+ apply (IlistPerm3_lgti H).
+ intro i1.
destruct (IlistPerm3_exists_rec H i1) as [i2 [Hyp1 Hyp2]].
exists i2.
split.
* exact Hyp1.
* apply IH.
-- apply Hyp2.
-- evalLgtiExtro.
apply Heqn.
Qed.
Lemma IlistPerm3_extroduce : forall (T: Set)(RelT: relation T)
(i1 i2: ilist T)(f1: Fin (lgti i1)) (f2 : Fin (lgti i2)), RelT (fcti i1 f1) (fcti i2 f2) ->
IlistPerm3 RelT (extroduce i1 f1) (extroduce i2 f2) -> IlistPerm3 RelT i1 i2.
Proof.
intros T RelT i1 i2 f1 f2.
apply IlistPerm3_cons.
Qed.
Lemma IlistPerm3_trans (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(l1 l2 l3 : ilist T) :
IlistPerm3 RelT l1 l2 -> IlistPerm3 RelT l2 l3 -> IlistPerm3 RelT l1 l3.
Proof.
intros H1 H2.
apply IlistPerm4_IlistPerm3_eq.
apply IlistPerm3_IlistPerm4_eq in H1.
apply IlistPerm3_IlistPerm4_eq in H2.
apply (IlistPerm4_trans _ H1 H2).
Qed.
Lemma IlistPerm3_trans_trans (T: Set)(RelT: relation T)(Rtrans: Transitive RelT)(l1 l2 l3 : ilist T) :
IlistPerm3 RelT l1 l2 -> IlistPerm3 RelT l2 l3 -> IlistPerm3 RelT l1 l3.
Proof.
intros H1 H2.
apply IlistPerm4_IlistPerm3_eq.
apply IlistPerm3_IlistPerm4_eq in H1.
apply IlistPerm3_IlistPerm4_eq in H2.
apply (IlistPerm4_trans_trans _ H1 H2).
Qed.
Add Parametric Relation (T: Set)(RelT: relation T)(EqT: Equivalence RelT) : (ilist T)(IlistPerm3 RelT)
reflexivity proved by (IlistPerm3_refl EqT)
symmetry proved by (IlistPerm3_sym EqT)
transitivity proved by (IlistPerm3_trans EqT)
as IlistPerm3Rel.
Lemma IlistPerm4_sym (T: Set)(RelT: relation T)(EqT: Equivalence RelT)(l1 l2 : ilist T) :
IlistPerm4 RelT l1 l2 -> IlistPerm4 RelT l2 l1.
Proof.
intros H1.
apply IlistPerm4_IlistPerm3_eq in H1.
apply IlistPerm3_IlistPerm4_eq.
apply (IlistPerm3_sym _ H1).
Qed.
Lemma IlistPerm4_sym_sym (T: Set)(RelT: relation T)(Rsym: Symmetric RelT)(l1 l2 : ilist T) :
IlistPerm4 RelT l1 l2 -> IlistPerm4 RelT l2 l1.
Proof.
intros H1.
apply IlistPerm4_IlistPerm3_eq in H1.
apply IlistPerm3_IlistPerm4_eq.
apply (IlistPerm3_sym_sym _ H1).
Qed.
Add Parametric Relation (T: Set)(RelT: relation T)(EqT: Equivalence RelT) : (ilist T)(IlistPerm4 RelT)
reflexivity proved by (IlistPerm4_refl EqT)
symmetry proved by (IlistPerm4_sym EqT)
transitivity proved by (IlistPerm4_trans EqT)
as IlistPerm4Rel.