summaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
blob: 9c23dda5efe0000898415a9ae4028f7199764d15 (plain)
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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
1933
1934
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
1954
1955
1956
1957
1958
1959
1960
1961
1962
1963
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: setoid_replace.ml 10213 2007-10-10 13:05:59Z letouzey $ *)

open Tacmach
open Proof_type
open Libobject
open Reductionops
open Term
open Termops
open Names
open Entries
open Libnames
open Nameops
open Util
open Pp
open Printer
open Environ
open Clenv
open Unification
open Tactics 
open Tacticals
open Vernacexpr
open Safe_typing
open Nametab
open Decl_kinds
open Constrintern
open Mod_subst

let replace = ref (fun _ _ _ -> assert false)
let register_replace f = replace := f

let general_rewrite = ref (fun _ _ -> assert false)
let register_general_rewrite f = general_rewrite := f

(* util function; it should be in util.mli *)
let prlist_with_sepi sep elem =
 let rec aux n =
  function
   | []   -> mt ()
   | [h]  -> elem n h
   | h::t ->
      let e = elem n h and s = sep() and r = aux (n+1) t in
      e ++ s ++ r
 in
  aux 1

type relation =
   { rel_a: constr ;
     rel_aeq: constr;
     rel_refl: constr option;
     rel_sym: constr option;
     rel_trans : constr option;
     rel_quantifiers_no: int  (* it helps unification *);
     rel_X_relation_class: constr;
     rel_Xreflexive_relation_class: constr
   }

type 'a relation_class =
   Relation of 'a            (* the rel_aeq of the relation or the relation   *)
 | Leibniz of constr option  (* the carrier (if eq is partially instantiated) *)

type 'a morphism =
    { args : (bool option * 'a relation_class) list;
      output : 'a relation_class;
      lem : constr;
      morphism_theory : constr
    }

type funct =
    { f_args : constr list;
      f_output : constr
    }

type morphism_class =
   ACMorphism of relation morphism
 | ACFunction of funct

let subst_mps_in_relation_class subst =
 function
    Relation  t -> Relation  (subst_mps subst t)
  | Leibniz t -> Leibniz (option_map (subst_mps subst) t) 

let subst_mps_in_argument_class subst (variance,rel) =
 variance, subst_mps_in_relation_class subst rel

let constr_relation_class_of_relation_relation_class =
 function
    Relation relation -> Relation relation.rel_aeq
  | Leibniz t -> Leibniz t
 

let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c

let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
let gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s
let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s
let eval_reference dir s = EvalConstRef (destConst (constant dir s))
let eval_init_reference dir s = EvalConstRef (destConst (gen_constant ("Init"::dir) s))

let current_constant id =
  try
    global_reference id
  with Not_found ->
    anomaly ("Setoid: cannot find " ^ (string_of_id id))

(* From Setoid.v *)

let coq_reflexive =
 lazy(gen_constant ["Relations"; "Relation_Definitions"] "reflexive")
let coq_symmetric =
 lazy(gen_constant ["Relations"; "Relation_Definitions"] "symmetric")
let coq_transitive =
 lazy(gen_constant ["Relations"; "Relation_Definitions"] "transitive")
let coq_relation =
 lazy(gen_constant ["Relations"; "Relation_Definitions"] "relation")

let coq_Relation_Class = lazy(constant ["Setoid"] "Relation_Class")
let coq_Argument_Class = lazy(constant ["Setoid"] "Argument_Class")
let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory")
let coq_Morphism_Theory = lazy(constant ["Setoid"] "Morphism_Theory")
let coq_Build_Morphism_Theory= lazy(constant ["Setoid"] "Build_Morphism_Theory")
let coq_Compat = lazy(constant ["Setoid"] "Compat")

let coq_AsymmetricReflexive = lazy(constant ["Setoid"] "AsymmetricReflexive")
let coq_SymmetricReflexive = lazy(constant ["Setoid"] "SymmetricReflexive")
let coq_SymmetricAreflexive = lazy(constant ["Setoid"] "SymmetricAreflexive")
let coq_AsymmetricAreflexive = lazy(constant ["Setoid"] "AsymmetricAreflexive")
let coq_Leibniz = lazy(constant ["Setoid"] "Leibniz")

let coq_RAsymmetric = lazy(constant ["Setoid"] "RAsymmetric")
let coq_RSymmetric = lazy(constant ["Setoid"] "RSymmetric")
let coq_RLeibniz = lazy(constant ["Setoid"] "RLeibniz")

let coq_ASymmetric = lazy(constant ["Setoid"] "ASymmetric")
let coq_AAsymmetric = lazy(constant ["Setoid"] "AAsymmetric")

let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl")
let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym")
let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans")

let coq_variance = lazy(constant ["Setoid"] "variance")
let coq_Covariant = lazy(constant ["Setoid"] "Covariant")
let coq_Contravariant = lazy(constant ["Setoid"] "Contravariant")
let coq_Left2Right = lazy(constant ["Setoid"] "Left2Right")
let coq_Right2Left = lazy(constant ["Setoid"] "Right2Left")
let coq_MSNone = lazy(constant ["Setoid"] "MSNone")
let coq_MSCovariant = lazy(constant ["Setoid"] "MSCovariant")
let coq_MSContravariant = lazy(constant ["Setoid"] "MSContravariant")

let coq_singl = lazy(constant ["Setoid"] "singl")
let coq_cons = lazy(constant ["Setoid"] "necons")

let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation =
 lazy(constant ["Setoid"]
  "equality_morphism_of_asymmetric_areflexive_transitive_relation")
let coq_equality_morphism_of_symmetric_areflexive_transitive_relation =
 lazy(constant ["Setoid"]
  "equality_morphism_of_symmetric_areflexive_transitive_relation")
let coq_equality_morphism_of_asymmetric_reflexive_transitive_relation =
 lazy(constant ["Setoid"]
  "equality_morphism_of_asymmetric_reflexive_transitive_relation")
let coq_equality_morphism_of_symmetric_reflexive_transitive_relation =
 lazy(constant ["Setoid"]
  "equality_morphism_of_symmetric_reflexive_transitive_relation")
let coq_make_compatibility_goal =
 lazy(constant ["Setoid"] "make_compatibility_goal")
let coq_make_compatibility_goal_eval_ref =
 lazy(eval_reference ["Setoid"] "make_compatibility_goal")
let coq_make_compatibility_goal_aux_eval_ref =
 lazy(eval_reference ["Setoid"] "make_compatibility_goal_aux")

let coq_App = lazy(constant ["Setoid"] "App")
let coq_ToReplace = lazy(constant ["Setoid"] "ToReplace")
let coq_ToKeep = lazy(constant ["Setoid"] "ToKeep")
let coq_ProperElementToKeep = lazy(constant ["Setoid"] "ProperElementToKeep")
let coq_fcl_singl = lazy(constant ["Setoid"] "fcl_singl")
let coq_fcl_cons = lazy(constant ["Setoid"] "fcl_cons")

let coq_setoid_rewrite = lazy(constant ["Setoid"] "setoid_rewrite")
let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
let coq_unit = lazy(gen_constant ["Init"; "Datatypes"] "unit")
let coq_tt = lazy(gen_constant ["Init"; "Datatypes"] "tt")
let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq")

let coq_morphism_theory_of_function =
 lazy(constant ["Setoid"] "morphism_theory_of_function")
let coq_morphism_theory_of_predicate =
 lazy(constant ["Setoid"] "morphism_theory_of_predicate")
let coq_relation_of_relation_class =
 lazy(eval_reference ["Setoid"] "relation_of_relation_class")
let coq_directed_relation_of_relation_class =
 lazy(eval_reference ["Setoid"] "directed_relation_of_relation_class")
let coq_interp = lazy(eval_reference ["Setoid"] "interp")
let coq_Morphism_Context_rect2 =
 lazy(eval_reference ["Setoid"] "Morphism_Context_rect2")
let coq_iff = lazy(gen_constant ["Init";"Logic"] "iff")
let coq_impl = lazy(constant ["Setoid"] "impl")


(************************* Table of declared relations **********************)


(* Relations are stored in a table which is synchronised with the Reset mechanism. *)

let relation_table = ref Gmap.empty

let relation_table_add (s,th) = relation_table := Gmap.add s th !relation_table
let relation_table_find s = Gmap.find s !relation_table
let relation_table_mem s = Gmap.mem s !relation_table

let prrelation s =
 str "(" ++ pr_lconstr s.rel_a ++ str "," ++ pr_lconstr s.rel_aeq ++ str ")"

let prrelation_class =
 function
    Relation eq  ->
     (try prrelation (relation_table_find eq)
      with Not_found ->
       str "[[ Error: " ++ pr_lconstr eq ++
        str " is not registered as a relation ]]")
  | Leibniz (Some ty) -> pr_lconstr ty
  | Leibniz None -> str "_"

let prmorphism_argument_gen prrelation (variance,rel) =
 prrelation rel ++
  match variance with
     None -> str " ==> "
   | Some true -> str " ++> "
   | Some false -> str " --> "

let prargument_class = prmorphism_argument_gen prrelation_class

let pr_morphism_signature (l,c) =
 prlist (prmorphism_argument_gen Ppconstr.pr_constr_expr) l ++
  Ppconstr.pr_constr_expr c

let prmorphism k m =
  pr_lconstr k ++ str ": " ++
  prlist prargument_class m.args ++
  prrelation_class m.output


(* A function that gives back the only relation_class on a given carrier *)
(*CSC: this implementation is really inefficient. I should define a new
  map to make it efficient. However, is this really worth of? *)
let default_relation_for_carrier ?(filter=fun _ -> true) a =
 let rng = Gmap.rng !relation_table in
 match List.filter (fun ({rel_a=rel_a} as r) -> rel_a = a && filter r) rng with
    [] -> Leibniz (Some a)
  | relation::tl ->
     if tl <> [] then
      ppnl
       (str "Warning: There are several relations on the carrier \"" ++
         pr_lconstr a ++ str "\". The relation " ++ prrelation relation ++
         str " is chosen.") ;
     Relation relation

let find_relation_class rel =
 try Relation (relation_table_find rel)
 with
  Not_found ->
   let rel = Reduction.whd_betadeltaiota (Global.env ()) rel in
   match kind_of_term rel with
    | App (eq,[|ty|]) when eq_constr eq (Lazy.force coq_eq) -> Leibniz (Some ty)
    | _ when eq_constr rel (Lazy.force coq_eq) -> Leibniz None
    | _ -> raise Not_found

let coq_iff_relation = lazy (find_relation_class (Lazy.force coq_iff))
let coq_impl_relation = lazy (find_relation_class (Lazy.force coq_impl))

let relation_morphism_of_constr_morphism =
 let relation_relation_class_of_constr_relation_class =
  function
     Leibniz t -> Leibniz t
   | Relation aeq ->
      Relation (try relation_table_find aeq with Not_found -> assert false)
 in
  function mor ->
   let args' =
    List.map
     (fun (variance,rel) ->
       variance, relation_relation_class_of_constr_relation_class rel
     ) mor.args in
   let output' = relation_relation_class_of_constr_relation_class mor.output in
    {mor with args=args' ; output=output'}

let subst_relation subst relation = 
  let rel_a' = subst_mps subst relation.rel_a in
  let rel_aeq' = subst_mps subst relation.rel_aeq in
  let rel_refl' = option_map (subst_mps subst) relation.rel_refl in
  let rel_sym' = option_map (subst_mps subst) relation.rel_sym in
  let rel_trans' = option_map (subst_mps subst) relation.rel_trans in
  let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in
  let rel_Xreflexive_relation_class' =
   subst_mps subst relation.rel_Xreflexive_relation_class
  in
    if rel_a' == relation.rel_a
      && rel_aeq' == relation.rel_aeq
      && rel_refl' == relation.rel_refl
      && rel_sym' == relation.rel_sym
      && rel_trans' == relation.rel_trans
      && rel_X_relation_class' == relation.rel_X_relation_class
      && rel_Xreflexive_relation_class'==relation.rel_Xreflexive_relation_class
    then
      relation
    else
      { rel_a = rel_a' ;
        rel_aeq = rel_aeq' ;
        rel_refl = rel_refl' ;
        rel_sym = rel_sym';
        rel_trans = rel_trans';
        rel_quantifiers_no = relation.rel_quantifiers_no;
        rel_X_relation_class = rel_X_relation_class';
        rel_Xreflexive_relation_class = rel_Xreflexive_relation_class'
      }
      
let equiv_list () = List.map (fun x -> x.rel_aeq) (Gmap.rng !relation_table)

let _ = 
  Summary.declare_summary "relation-table"
    { Summary.freeze_function = (fun () -> !relation_table);
      Summary.unfreeze_function = (fun t -> relation_table := t);
      Summary.init_function = (fun () -> relation_table := Gmap .empty);
      Summary.survive_module = false;
      Summary.survive_section = false }

(* Declare a new type of object in the environment : "relation-theory". *)

let (relation_to_obj, obj_to_relation)=
  let cache_set (_,(s, th)) =
   let th' =
    if relation_table_mem s then
     begin
      let old_relation = relation_table_find s in
       let th' =
        {th with rel_sym =
          match th.rel_sym with
             None -> old_relation.rel_sym
           | Some t -> Some t} in
        ppnl
         (str "Warning: The relation " ++ prrelation th' ++
          str " is redeclared. The new declaration" ++
           (match th'.rel_refl with
              None -> str ""
            | Some t -> str " (reflevity proved by " ++ pr_lconstr t) ++
           (match th'.rel_sym with
               None -> str ""
             | Some t ->
                (if th'.rel_refl = None then str " (" else str " and ") ++
                str "symmetry proved by " ++ pr_lconstr t) ++
           (if th'.rel_refl <> None && th'.rel_sym <> None then
             str ")" else str "") ++
           str " replaces the old declaration" ++
           (match old_relation.rel_refl with
              None -> str ""
            | Some t -> str " (reflevity proved by " ++ pr_lconstr t) ++
           (match old_relation.rel_sym with
               None -> str ""
             | Some t ->
                (if old_relation.rel_refl = None then
                  str " (" else str " and ") ++
                str "symmetry proved by " ++ pr_lconstr t) ++
           (if old_relation.rel_refl <> None && old_relation.rel_sym <> None
            then str ")" else str "") ++
           str ".");
        th'
     end
    else
     th
   in
    relation_table_add (s,th')
  and subst_set (_,subst,(s,th as obj)) =
    let s' = subst_mps subst s in
    let th' = subst_relation subst th in
      if s' == s && th' == th then obj else
        (s',th')
  and export_set x = Some x 
  in 
    declare_object {(default_object "relation-theory") with
                      cache_function = cache_set;
                      load_function = (fun i o -> cache_set o);
                      subst_function = subst_set;
                      classify_function = (fun (_,x) -> Substitute x);
                      export_function = export_set}

(******************************* Table of declared morphisms ********************)

(* Setoids are stored in a table which is synchronised with the Reset mechanism. *)

let morphism_table = ref Gmap.empty

let morphism_table_find m = Gmap.find m !morphism_table
let morphism_table_add (m,c) =
 let old =
  try
   morphism_table_find m
  with
   Not_found -> []
 in
  try
   let old_morph =
    List.find
     (function mor -> mor.args = c.args && mor.output = c.output) old
   in
    ppnl
     (str "Warning: The morphism " ++ prmorphism m old_morph ++
      str " is redeclared. " ++
      str "The new declaration whose compatibility is proved by " ++
       pr_lconstr c.lem ++ str " replaces the old declaration whose" ++
       str " compatibility was proved by " ++
       pr_lconstr old_morph.lem ++ str ".")
  with
   Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table

let default_morphism ?(filter=fun _ -> true) m =
  match List.filter filter (morphism_table_find m) with
      [] -> raise Not_found
    | m1::ml ->
        if ml <> [] then
          ppnl
            (str "Warning: There are several morphisms associated to \"" ++
            pr_lconstr m ++ str"\". Morphism " ++ prmorphism m m1 ++
            str " is randomly chosen.");
        relation_morphism_of_constr_morphism m1

let subst_morph subst morph = 
  let lem' = subst_mps subst morph.lem in
  let args' = list_smartmap (subst_mps_in_argument_class subst) morph.args in
  let output' = subst_mps_in_relation_class subst morph.output in
  let morphism_theory' = subst_mps subst morph.morphism_theory in
    if lem' == morph.lem
      && args' == morph.args
      && output' == morph.output
      && morphism_theory' == morph.morphism_theory
    then
      morph
    else
      { args = args' ;
        output = output' ;
        lem = lem' ;
        morphism_theory = morphism_theory'
      }


let _ = 
  Summary.declare_summary "morphism-table"
    { Summary.freeze_function = (fun () -> !morphism_table);
      Summary.unfreeze_function = (fun t -> morphism_table := t);
      Summary.init_function = (fun () -> morphism_table := Gmap .empty);
      Summary.survive_module = false;
      Summary.survive_section = false }

(* Declare a new type of object in the environment : "morphism-definition". *)

let (morphism_to_obj, obj_to_morphism)=
  let cache_set (_,(m, c)) = morphism_table_add (m, c)
  and subst_set (_,subst,(m,c as obj)) = 
    let m' = subst_mps subst m in
    let c' = subst_morph subst c in
      if m' == m && c' == c then obj else
        (m',c')
  and export_set x = Some x 
  in 
    declare_object {(default_object "morphism-definition") with
                      cache_function = cache_set;
                      load_function = (fun i o -> cache_set o);
                      subst_function = subst_set;
                      classify_function = (fun (_,x) -> Substitute x);
                      export_function = export_set}

(************************** Printing relations and morphisms **********************)

let print_setoids () =
  Gmap.iter
   (fun k relation ->
     assert (k=relation.rel_aeq) ;
     ppnl (str"Relation " ++ prrelation relation ++ str";" ++
      (match relation.rel_refl with
          None -> str ""
        | Some t -> str" reflexivity proved by " ++ pr_lconstr t) ++
      (match relation.rel_sym with
          None -> str ""
        | Some t -> str " symmetry proved by " ++ pr_lconstr t) ++
      (match relation.rel_trans with
          None -> str ""
        | Some t -> str " transitivity proved by " ++ pr_lconstr t)))
   !relation_table ;
  Gmap.iter
   (fun k l ->
     List.iter
      (fun ({lem=lem} as mor) ->
        ppnl (str "Morphism " ++ prmorphism k mor ++
        str ". Compatibility proved by " ++
        pr_lconstr lem ++ str "."))
      l) !morphism_table
;;

(***************** Adding a morphism to the database ****************************)

(* We maintain a table of the currently edited proofs of morphism lemma
   in order to add them in the morphism_table when the user does Save *)

let edited = ref Gmap.empty

let new_edited id m = 
  edited := Gmap.add id m !edited

let is_edited id =
  Gmap.mem id !edited

let no_more_edited id =
  edited := Gmap.remove id !edited

let what_edited id =
  Gmap.find id !edited

(* also returns the triple (args_ty_quantifiers_rev,real_args_ty,real_output)
   where the args_ty and the output are delifted *)
let check_is_dependent n args_ty output =
 let m = List.length args_ty - n in
 let args_ty_quantifiers, args_ty = Util.list_chop n args_ty in
  let rec aux m t =
   match kind_of_term t with
      Prod (n,s,t) when m > 0 ->
       if not (dependent (mkRel 1) t) then
        let args,out = aux (m - 1) (subst1 (mkRel 1) (* dummy *) t) in
         s::args,out
       else
        errorlabstrm "New Morphism"
         (str "The morphism is not a quantified non dependent product.")
    | _ -> [],t
  in
   let ty = compose_prod (List.rev args_ty) output in
   let args_ty, output = aux m ty in
   List.rev args_ty_quantifiers, args_ty, output

let cic_relation_class_of_X_relation typ value =
 function
    {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} ->
     mkApp ((Lazy.force coq_AsymmetricReflexive),
      [| typ ; value ; rel_a ; rel_aeq; refl |])
  | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} ->
     mkApp ((Lazy.force coq_SymmetricReflexive),
      [| typ ; rel_a ; rel_aeq; sym ; refl |])
  | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} ->
     mkApp ((Lazy.force coq_AsymmetricAreflexive),
      [| typ ; value ; rel_a ; rel_aeq |])
  | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} ->
     mkApp ((Lazy.force coq_SymmetricAreflexive),
      [| typ ; rel_a ; rel_aeq; sym |])

let cic_relation_class_of_X_relation_class typ value =
 function
    Relation {rel_X_relation_class=x_relation_class} ->
     mkApp (x_relation_class, [| typ ; value |])
  | Leibniz (Some t) ->
     mkApp ((Lazy.force coq_Leibniz), [| typ ; t |])
  | Leibniz None -> assert false


let cic_precise_relation_class_of_relation =
 function
    {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} ->
      mkApp ((Lazy.force coq_RAsymmetric), [| rel_a ; rel_aeq; refl |])
  | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} ->
      mkApp ((Lazy.force coq_RSymmetric), [| rel_a ; rel_aeq; sym ; refl |])
  | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} ->
      mkApp ((Lazy.force coq_AAsymmetric), [| rel_a ; rel_aeq |])
  | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} ->
      mkApp ((Lazy.force coq_ASymmetric), [| rel_a ; rel_aeq; sym |])

let cic_precise_relation_class_of_relation_class =
 function
    Relation
     {rel_aeq=rel_aeq; rel_Xreflexive_relation_class=lem; rel_refl=rel_refl }
     ->
      rel_aeq,lem,not(rel_refl=None)
  | Leibniz (Some t) ->
     mkApp ((Lazy.force coq_eq), [| t |]),
      mkApp ((Lazy.force coq_RLeibniz), [| t |]), true
  | Leibniz None -> assert false

let cic_relation_class_of_relation_class rel =
 cic_relation_class_of_X_relation_class
  (Lazy.force coq_unit) (Lazy.force coq_tt) rel

let cic_argument_class_of_argument_class (variance,arg) =
 let coq_variant_value =
  match variance with
     None -> (Lazy.force coq_Covariant) (* dummy value, it won't be used *)
   | Some true -> (Lazy.force coq_Covariant)
   | Some false -> (Lazy.force coq_Contravariant)
 in
  cic_relation_class_of_X_relation_class (Lazy.force coq_variance)
   coq_variant_value arg

let cic_arguments_of_argument_class_list args =
 let rec aux =
  function
     [] -> assert false
   | [last] ->
      mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class; last |])
   | he::tl ->
      mkApp ((Lazy.force coq_cons),
       [| Lazy.force coq_Argument_Class; he ; aux tl |])
 in
  aux (List.map cic_argument_class_of_argument_class args)

let gen_compat_lemma_statement quantifiers_rev output args m =
 let output = cic_relation_class_of_relation_class output in
 let args = cic_arguments_of_argument_class_list args in
  args, output,
   compose_prod quantifiers_rev
    (mkApp ((Lazy.force coq_make_compatibility_goal), [| args ; output ; m |]))

let morphism_theory_id_of_morphism_proof_id id =
 id_of_string (string_of_id id ^ "_morphism_theory")

(* apply_to_rels c [l1 ; ... ; ln] returns (c Rel1 ... reln) *)
let apply_to_rels c l =
 if l = [] then c
 else
  let len = List.length l in
   applistc c (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 l)

let apply_to_relation subst rel =
 if Array.length subst = 0 then rel
 else
  let new_quantifiers_no = rel.rel_quantifiers_no - Array.length subst in
   assert (new_quantifiers_no >= 0) ;
   { rel_a = mkApp (rel.rel_a, subst) ;
     rel_aeq = mkApp (rel.rel_aeq, subst) ;
     rel_refl = option_map (fun c -> mkApp (c,subst)) rel.rel_refl ; 
     rel_sym = option_map (fun c -> mkApp (c,subst)) rel.rel_sym;
     rel_trans = option_map (fun c -> mkApp (c,subst)) rel.rel_trans;
     rel_quantifiers_no = new_quantifiers_no;
     rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst);
     rel_Xreflexive_relation_class =
      mkApp (rel.rel_Xreflexive_relation_class, subst) }

let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
 let lem =
  match lemma_infos with
     None ->
      (* the Morphism_Theory object has already been created *)
      let applied_args =
       let len = List.length quantifiers_rev in
       let subst =
        Array.of_list
         (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 quantifiers_rev)
       in
        List.map
         (fun (v,rel) ->
           match rel with
              Leibniz (Some t) ->
               assert (subst=[||]);
               v, Leibniz (Some t)
            | Leibniz None ->
               assert (Array.length subst = 1);
               v, Leibniz (Some (subst.(0)))
            | Relation rel -> v, Relation (apply_to_relation subst rel)) args
      in
       compose_lam quantifiers_rev
        (mkApp (Lazy.force coq_Compat,
          [| cic_arguments_of_argument_class_list applied_args;
             cic_relation_class_of_relation_class output;
             apply_to_rels (current_constant mor_name) quantifiers_rev |]))
   | Some (lem_name,argsconstr,outputconstr) ->
      (* only the compatibility has been proved; we need to declare the
         Morphism_Theory object *)
     let mext = current_constant lem_name in
     ignore (
      Declare.declare_internal_constant mor_name
       (DefinitionEntry
         {const_entry_body =
           compose_lam quantifiers_rev
            (mkApp ((Lazy.force coq_Build_Morphism_Theory),
              [| argsconstr; outputconstr; apply_to_rels m quantifiers_rev ;
                  apply_to_rels mext quantifiers_rev |]));
          const_entry_type = None;
          const_entry_opaque = false;
          const_entry_boxed = Options.boxed_definitions()},
	IsDefinition Definition)) ;
     mext 
 in
  let mmor = current_constant mor_name in
  let args_constr =
   List.map
    (fun (variance,arg) ->
      variance, constr_relation_class_of_relation_relation_class arg) args in
  let output_constr = constr_relation_class_of_relation_relation_class output in
   Lib.add_anonymous_leaf
    (morphism_to_obj (m, 
      { args = args_constr;
        output = output_constr;
        lem = lem;
        morphism_theory = mmor }));
   Options.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism")   

(* first order matching with a bit of conversion *)
let unify_relation_carrier_with_type env rel t =
 let raise_error quantifiers_no =
  errorlabstrm "New Morphism"
   (str "One morphism argument or its output has type " ++ 
    pr_lconstr_env env t ++
    str " but the signature requires an argument of type \"" ++
    pr_lconstr_env env rel.rel_a ++ prvect_with_sep mt (fun _ -> str " ?")
     (Array.make quantifiers_no 0) ++ str "\"") in
 let args =
  match kind_of_term t with
     App (he',args') ->
      let argsno = Array.length args' - rel.rel_quantifiers_no in
      let args1 = Array.sub args' 0 argsno in
      let args2 = Array.sub args' argsno rel.rel_quantifiers_no in
       if is_conv env Evd.empty rel.rel_a (mkApp (he',args1)) then
        args2
       else
        raise_error rel.rel_quantifiers_no
   | _  ->
     if rel.rel_quantifiers_no = 0 && is_conv env Evd.empty rel.rel_a t then
      [||] 
     else
      begin
        let evars,args,instantiated_rel_a =
         let ty = Typing.type_of env Evd.empty rel.rel_a in
         let evd = Evd.create_evar_defs Evd.empty in
         let evars,args,concl =
          Clenv.clenv_environments_evars env evd
           (Some rel.rel_quantifiers_no) ty
         in
          evars, args,
          nf_betaiota
           (match args with [] -> rel.rel_a | _ -> applist (rel.rel_a,args))
        in
         let evars' =
          w_unify true (*??? or false? *) env Reduction.CONV (*??? or cumul? *)
           ~mod_delta:true (*??? or true? *) t instantiated_rel_a evars in
         let args' =
          List.map (Reductionops.nf_evar (Evd.evars_of evars')) args
         in
          Array.of_list args'
      end
 in
  apply_to_relation args rel

let unify_relation_class_carrier_with_type env rel t =
 match rel with
    Leibniz (Some t') ->
     if is_conv env Evd.empty t t' then
      rel
     else
      errorlabstrm "New Morphism"
       (str "One morphism argument or its output has type " ++ 
        pr_lconstr_env env t ++
        str " but the signature requires an argument of type " ++
        pr_lconstr_env env t')
  | Leibniz None -> Leibniz (Some t)
  | Relation rel -> Relation (unify_relation_carrier_with_type env rel t)

exception Impossible

(* first order matching with a bit of conversion *)
(* Note: the type checking operations performed by the function could  *)
(* be done once and for all abstracting the morphism structure using   *)
(* the quantifiers. Would the new structure be more suited than the    *)
(* existent one for other tasks to? (e.g. pretty printing would expose *)
(* much more information: is it ok or is it too much information?)     *)
let unify_morphism_with_arguments gl (c,av)
     {args=args; output=output; lem=lem; morphism_theory=morphism_theory} t
=
 let avlen = Array.length av in 
 let argsno = List.length args in
 if avlen < argsno then raise Impossible; (* partial application *)
 let al = Array.to_list av in
 let quantifiers,al' = Util.list_chop (avlen - argsno) al in
 let quantifiersv = Array.of_list quantifiers in
 let c' = mkApp (c,quantifiersv) in
 if dependent t c' then raise Impossible; 
 (* these are pf_type_of we could avoid *)
 let al'_type = List.map (Tacmach.pf_type_of gl) al' in
 let args' =
   List.map2
     (fun (var,rel) ty ->
	var,unify_relation_class_carrier_with_type (pf_env gl) rel ty)
     args al'_type in
 (* this is another pf_type_of we could avoid *)
 let ty = Tacmach.pf_type_of gl (mkApp (c,av)) in
 let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty in
 let lem' = mkApp (lem,quantifiersv) in
 let morphism_theory' = mkApp (morphism_theory,quantifiersv) in
 ({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'},
  c',Array.of_list al')

let new_morphism m signature id hook =
 if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
  errorlabstrm "New Morphism" (pr_id id ++ str " already exists")
 else
  let env = Global.env() in
  let typeofm = Typing.type_of env Evd.empty m in
  let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in
  let argsrev, output =
    match signature with
	None -> decompose_prod typ
      | Some (_,output') ->
	  (* the carrier of the relation output' can be a Prod ==>
             we must uncurry on the fly output.
             E.g: A -> B -> C vs        A -> (B -> C)
             args   output     args     output
	  *)
	  let rel = 
	    try find_relation_class output' 
	    with Not_found -> errorlabstrm "Add Morphism"
	      (str "Not a valid signature: " ++ pr_lconstr output' ++
		 str " is neither a registered relation nor the Leibniz " ++
		 str " equality.") in
	  let rel_a,rel_quantifiers_no =
            match rel with
		Relation rel -> rel.rel_a, rel.rel_quantifiers_no
              | Leibniz (Some t) -> t, 0
              | Leibniz None -> let _,t = decompose_prod typ in t, 0 in
	  let rel_a_n =
            clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a 
	  in
	    try
              let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in
              let argsrev,_ = decompose_prod output_rel_a_n in
              let n = List.length argsrev in
              let argsrev',_ = decompose_prod typ in
              let m = List.length argsrev' in
		decompose_prod_n (m - n) typ
	    with UserError(_,_) ->
              (* decompose_lam_n failed. This may happen when rel_a is an axiom,
		 a constructor, an inductive type, etc. *)
              decompose_prod typ
  in
  let args_ty = List.rev argsrev in
  let args_ty_len = List.length (args_ty) in
  let args_ty_quantifiers_rev,args,args_instance,output,output_instance =
    match signature with
	None ->
	  if args_ty = [] then
            errorlabstrm "New Morphism"
              (str "The term " ++ pr_lconstr m ++ str " has type " ++
		  pr_lconstr typeofm ++ str " that is not a product.") ;
	  ignore (check_is_dependent 0 args_ty output) ;
	  let args =
            List.map
              (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in
	  let output = default_relation_for_carrier output in
            [],args,args,output,output
      | Some (args,output') ->
	  assert (args <> []);
	  let number_of_arguments = List.length args in
	  let number_of_quantifiers = args_ty_len - number_of_arguments in
	    if number_of_quantifiers < 0 then
              errorlabstrm "New Morphism"
		(str "The morphism " ++ pr_lconstr m ++ str " has type " ++
		    pr_lconstr typeofm ++ str " that attends at most " ++ int args_ty_len ++
		    str " arguments. The signature that you specified requires " ++
		    int number_of_arguments ++ str " arguments.")
	    else
              begin
		(* the real_args_ty returned are already delifted *)
		let args_ty_quantifiers_rev, real_args_ty, real_output =
		  check_is_dependent number_of_quantifiers args_ty output in
		let quantifiers_rel_context =
		  List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in
		let env = push_rel_context quantifiers_rel_context env in
		let find_relation_class t real_t =
		  try
		    let rel = find_relation_class t in
		      rel, unify_relation_class_carrier_with_type env rel real_t
		  with Not_found ->
		    errorlabstrm "Add Morphism"
		      (str "Not a valid signature: " ++ pr_lconstr t ++
			  str " is neither a registered relation nor the Leibniz " ++
			  str " equality.")
		in
		let find_relation_class_v (variance,t) real_t =
		  let relation,relation_instance = find_relation_class t real_t in
		    match relation, variance with
			Leibniz _, None
		      | Relation {rel_sym = Some _}, None
		      | Relation {rel_sym = None}, Some _ ->
			  (variance, relation), (variance, relation_instance)
		      | Relation {rel_sym = None},None ->
			  errorlabstrm "Add Morphism"
			    (str "You must specify the variance in each argument " ++
				str "whose relation is asymmetric.")
		      | Leibniz _, Some _
		      | Relation {rel_sym = Some _}, Some _ ->
			  errorlabstrm "Add Morphism"
			    (str "You cannot specify the variance of an argument " ++
				str "whose relation is symmetric.")
		in
		let args, args_instance =
		  List.split
		    (List.map2 find_relation_class_v args real_args_ty) in
		let output,output_instance= find_relation_class output' real_output in
		  args_ty_quantifiers_rev, args, args_instance, output, output_instance
              end
  in
  let argsconstr,outputconstr,lem =
    gen_compat_lemma_statement args_ty_quantifiers_rev output_instance
      args_instance (apply_to_rels m args_ty_quantifiers_rev) in
    (* "unfold make_compatibility_goal" *)
  let lem =
    Reductionops.clos_norm_flags
      (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref))
      env Evd.empty lem in
    (* "unfold make_compatibility_goal_aux" *)
  let lem =
    Reductionops.clos_norm_flags
      (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref))
      env Evd.empty lem in
    (* "simpl" *)
  let lem = Tacred.nf env Evd.empty lem in
    if Lib.is_modtype () then
      begin
	ignore
	  (Declare.declare_internal_constant id
              (ParameterEntry lem, IsAssumption Logical)) ;
	let mor_name = morphism_theory_id_of_morphism_proof_id id in
	let lemma_infos = Some (id,argsconstr,outputconstr) in
	  add_morphism lemma_infos mor_name
            (m,args_ty_quantifiers_rev,args,output)
      end
    else
      begin
	new_edited id
	  (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
	Pfedit.start_proof id (Global, Proof Lemma) 
	  (Declare.clear_proofs (Global.named_context ()))
	  lem hook;
	Options.if_verbose msg (Printer.pr_open_subgoals ());
      end

let morphism_hook _ ref =
  let pf_id = id_of_global ref in
  let mor_id = morphism_theory_id_of_morphism_proof_id pf_id in
  let (m,quantifiers_rev,args,argsconstr,output,outputconstr) =
   what_edited pf_id in
  if (is_edited pf_id)
  then 
   begin
    add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id
     (m,quantifiers_rev,args,output) ;
    no_more_edited pf_id
   end

type morphism_signature =
 (bool option * Topconstr.constr_expr) list * Topconstr.constr_expr

let new_named_morphism id m sign =
 let sign =
  match sign with
     None -> None
   | Some (args,out) ->
      if args = [] then
	error "Morphism signature expects at least one argument.";
      Some
       (List.map (fun (variance,ty) -> variance, constr_of ty) args,
        constr_of out)
 in
  new_morphism (constr_of m) sign id morphism_hook

(************************** Adding a relation to the database *********************)

let check_a env a =
 let typ = Typing.type_of env Evd.empty a in
 let a_quantifiers_rev,_ = Reduction.dest_arity env typ in
  a_quantifiers_rev

let check_eq env a_quantifiers_rev a aeq =
 let typ =
  Sign.it_mkProd_or_LetIn
   (mkApp ((Lazy.force coq_relation),[| apply_to_rels a a_quantifiers_rev |]))
   a_quantifiers_rev in
 if
  not
   (is_conv env Evd.empty (Typing.type_of env Evd.empty aeq) typ)
 then
  errorlabstrm "Add Relation Class"
   (pr_lconstr aeq ++ str " should have type (" ++ pr_lconstr typ ++ str ")")

let check_property env a_quantifiers_rev a aeq strprop coq_prop t =
 if
  not
   (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
    (Sign.it_mkProd_or_LetIn
     (mkApp ((Lazy.force coq_prop),
       [| apply_to_rels a   a_quantifiers_rev ;
          apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev))
 then
  errorlabstrm "Add Relation Class"
   (str "Not a valid proof of " ++ str strprop ++ str ".")

let check_refl env a_quantifiers_rev a aeq refl =
 check_property env a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl

let check_sym env a_quantifiers_rev a aeq sym =
 check_property env a_quantifiers_rev a aeq "symmetry" coq_symmetric sym

let check_trans env a_quantifiers_rev a aeq trans =
 check_property env a_quantifiers_rev a aeq "transitivity" coq_transitive trans

let check_setoid_theory env a_quantifiers_rev a aeq th =
 if
  not
   (is_conv env Evd.empty (Typing.type_of env Evd.empty th)
    (Sign.it_mkProd_or_LetIn
     (mkApp ((Lazy.force coq_Setoid_Theory),
       [| apply_to_rels a   a_quantifiers_rev ;
          apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev))
 then
  errorlabstrm "Add Relation Class"
   (str "Not a valid proof of symmetry")

let int_add_relation id a aeq refl sym trans =
 let env = Global.env () in
 let a_quantifiers_rev = check_a env a in
  check_eq env a_quantifiers_rev a aeq  ;
  option_iter (check_refl env a_quantifiers_rev a aeq) refl ;
  option_iter (check_sym env a_quantifiers_rev a aeq) sym ;
  option_iter (check_trans env a_quantifiers_rev a aeq) trans ;
  let quantifiers_no = List.length a_quantifiers_rev in
  let aeq_rel =
   { rel_a = a;
     rel_aeq = aeq;
     rel_refl = refl;
     rel_sym = sym;
     rel_trans = trans;
     rel_quantifiers_no = quantifiers_no;
     rel_X_relation_class = mkProp; (* dummy value, overwritten below *)
     rel_Xreflexive_relation_class = mkProp (* dummy value, overwritten below *)
   } in
  let x_relation_class =
   let subst =
    let len = List.length a_quantifiers_rev in
    Array.of_list
     (Util.list_map_i (fun i _ -> mkRel (len - i + 2)) 0 a_quantifiers_rev) in
   cic_relation_class_of_X_relation
    (mkRel 2) (mkRel 1) (apply_to_relation subst aeq_rel) in
  let _ =
   Declare.declare_internal_constant id
    (DefinitionEntry
      {const_entry_body =
        Sign.it_mkLambda_or_LetIn x_relation_class
         ([ Name (id_of_string "v"),None,mkRel 1;
            Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @
            a_quantifiers_rev);
       const_entry_type = None;
       const_entry_opaque = false;
       const_entry_boxed = Options.boxed_definitions()},
      IsDefinition Definition) in
  let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in
  let xreflexive_relation_class =
   let subst =
    let len = List.length a_quantifiers_rev in
    Array.of_list
     (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 a_quantifiers_rev)
   in
    cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in
  let _ =
   Declare.declare_internal_constant id_precise
    (DefinitionEntry
      {const_entry_body =
        Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
       const_entry_type = None;
       const_entry_opaque = false;
       const_entry_boxed = Options.boxed_definitions() },
      IsDefinition Definition) in
  let aeq_rel =
   { aeq_rel with
      rel_X_relation_class = current_constant id;
      rel_Xreflexive_relation_class = current_constant id_precise } in
  Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ;
  Options.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation");
  match trans with
     None -> ()
   | Some trans ->
      let mor_name = id_of_string (string_of_id id ^ "_morphism") in
      let a_instance = apply_to_rels a a_quantifiers_rev in
      let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
      let sym_instance =
       option_map (fun x -> apply_to_rels x a_quantifiers_rev) sym in
      let refl_instance =
       option_map (fun x -> apply_to_rels x a_quantifiers_rev) refl in
      let trans_instance = apply_to_rels trans a_quantifiers_rev in
      let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output =
       match sym_instance, refl_instance with
          None, None ->
           (Some false, Relation aeq_rel),
           (Some true, Relation aeq_rel),
            mkApp
             ((Lazy.force
                coq_equality_morphism_of_asymmetric_areflexive_transitive_relation),
              [| a_instance ; aeq_instance ; trans_instance |]),
            Lazy.force coq_impl_relation
        | None, Some refl_instance ->
           (Some false, Relation aeq_rel),
           (Some true, Relation aeq_rel),
            mkApp
             ((Lazy.force
                coq_equality_morphism_of_asymmetric_reflexive_transitive_relation),
              [| a_instance ; aeq_instance ; refl_instance ; trans_instance |]),
            Lazy.force coq_impl_relation
        | Some sym_instance, None ->
           (None, Relation aeq_rel),
           (None, Relation aeq_rel),
            mkApp
             ((Lazy.force
                coq_equality_morphism_of_symmetric_areflexive_transitive_relation),
              [| a_instance ; aeq_instance ; sym_instance ; trans_instance |]),
            Lazy.force coq_iff_relation
        | Some sym_instance, Some refl_instance ->
           (None, Relation aeq_rel),
           (None, Relation aeq_rel),
            mkApp
             ((Lazy.force
                coq_equality_morphism_of_symmetric_reflexive_transitive_relation),
              [| a_instance ; aeq_instance ; refl_instance ; sym_instance ;
                 trans_instance |]),
            Lazy.force coq_iff_relation in
      let _ =
       Declare.declare_internal_constant mor_name
        (DefinitionEntry
          {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev;
           const_entry_type = None;
           const_entry_opaque = false;
          const_entry_boxed = Options.boxed_definitions()},
          IsDefinition Definition)
      in
       let a_quantifiers_rev =
        List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
       add_morphism None mor_name
        (aeq,a_quantifiers_rev,[aeq_rel_class_and_var1; aeq_rel_class_and_var2],
          output)

(* The vernac command "Add Relation ..." *)
let add_relation id a aeq refl sym trans =
 int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl)
  (option_map constr_of sym) (option_map constr_of trans)

(************************ Add Setoid ******************************************)

(* The vernac command "Add Setoid" *)
let add_setoid id a aeq th =
 let a = constr_of a in
 let aeq = constr_of aeq in
 let th = constr_of th in
 let env = Global.env () in
 let a_quantifiers_rev = check_a env a in
  check_eq env a_quantifiers_rev a aeq  ;
  check_setoid_theory env a_quantifiers_rev a aeq  th ;
   let a_instance = apply_to_rels a a_quantifiers_rev in
   let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
   let th_instance = apply_to_rels th a_quantifiers_rev in
   let refl =
    Sign.it_mkLambda_or_LetIn
     (mkApp ((Lazy.force coq_seq_refl),
       [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
   let sym =
    Sign.it_mkLambda_or_LetIn
     (mkApp ((Lazy.force coq_seq_sym),
       [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
   let trans =
    Sign.it_mkLambda_or_LetIn
     (mkApp ((Lazy.force coq_seq_trans),
       [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
   int_add_relation id a aeq (Some refl) (Some sym) (Some trans)


(****************************** The tactic itself *******************************)

type direction =
   Left2Right
 | Right2Left

let prdirection =
 function
    Left2Right -> str "->"
  | Right2Left -> str "<-"

type constr_with_marks =
  | MApp of constr * morphism_class * constr_with_marks array * direction
  | ToReplace
  | ToKeep of constr * relation relation_class * direction

let is_to_replace = function
 | ToKeep _ -> false
 | ToReplace -> true
 | MApp _ -> true

let get_mark a = 
  Array.fold_left (||) false (Array.map is_to_replace a)

let cic_direction_of_direction =
 function
    Left2Right -> Lazy.force coq_Left2Right
  | Right2Left -> Lazy.force coq_Right2Left

let opposite_direction =
 function
    Left2Right -> Right2Left
  | Right2Left -> Left2Right

let direction_of_constr_with_marks hole_direction =
 function
    MApp (_,_,_,dir) -> cic_direction_of_direction dir
  | ToReplace -> hole_direction
  | ToKeep (_,_,dir) -> cic_direction_of_direction dir

type argument =
   Toapply of constr         (* apply the function to the argument *)
 | Toexpand of name * types  (* beta-expand the function w.r.t. an argument
                                of this type *)
let beta_expand c args_rev =
 let rec to_expand =
  function
     [] -> []
   | (Toapply _)::tl -> to_expand tl
   | (Toexpand (name,s))::tl -> (name,s)::(to_expand tl) in
 let rec aux n =
  function
     [] -> []
   | (Toapply arg)::tl -> arg::(aux n tl)
   | (Toexpand _)::tl -> (mkRel n)::(aux (n + 1) tl)
 in
  compose_lam (to_expand args_rev)
   (mkApp (c, Array.of_list (List.rev (aux 1 args_rev))))

exception Optimize (* used to fall-back on the tactic for Leibniz equality *)

let relation_class_that_matches_a_constr caller_name new_goals hypt =
 let (heq, hargs) = decompose_app hypt in
 let rec get_all_but_last_two =
  function
     []
   | [_] ->
      errorlabstrm caller_name (pr_lconstr hypt ++
       str " is not a registered relation.")
   | [_;_] -> []
   | he::tl -> he::(get_all_but_last_two tl) in
 let all_aeq_args = get_all_but_last_two hargs in
 let rec find_relation l subst =
  let aeq = mkApp (heq,(Array.of_list l)) in
  try
   let rel = find_relation_class aeq in
   match rel,new_goals with
      Leibniz _,[] ->
       assert (subst = []);
       raise Optimize (* let's optimize the proof term size *)
    | Leibniz (Some _), _ ->
       assert (subst = []);
       rel
    | Leibniz None, _ ->
       (* for well-typedness reasons it should have been catched by the
          previous guard in the previous iteration. *)
       assert false
    | Relation rel,_ -> Relation (apply_to_relation (Array.of_list subst) rel)
  with Not_found ->
   if l = [] then
    errorlabstrm caller_name
     (pr_lconstr (mkApp (aeq, Array.of_list all_aeq_args)) ++
      str " is not a registered relation.")
   else
    let last,others = Util.list_sep_last l in
    find_relation others (last::subst)
 in
  find_relation all_aeq_args []

(* rel1 is a subrelation of rel2 whenever 
    forall x1 x2, rel1 x1 x2 -> rel2 x1 x2
   The Coq part of the tactic, however, needs rel1 == rel2.
   Hence the third case commented out.
   Note: accepting user-defined subrelations seems to be the last
   useful generalization that does not go against the original spirit of
   the tactic.
*)
let subrelation gl rel1 rel2 =
 match rel1,rel2 with
    Relation {rel_aeq=rel_aeq1}, Relation {rel_aeq=rel_aeq2} ->
     Tacmach.pf_conv_x gl rel_aeq1 rel_aeq2
  | Leibniz (Some t1), Leibniz (Some t2) ->
     Tacmach.pf_conv_x gl t1 t2
  | Leibniz None, _
  | _, Leibniz None -> assert false
(* This is the commented out case (see comment above)
  | Leibniz (Some t1), Relation {rel_a=t2; rel_refl = Some _} ->
     Tacmach.pf_conv_x gl t1 t2
*)
  | _,_ -> false

(* this function returns the list of new goals opened by a constr_with_marks *)
let rec collect_new_goals =
 function
   MApp (_,_,a,_) -> List.concat (List.map collect_new_goals (Array.to_list a))
 | ToReplace
 | ToKeep (_,Leibniz _,_)
 | ToKeep (_,Relation {rel_refl=Some _},_) -> []
 | ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) -> [mkApp(aeq,[|c ; c|])]

(* two marked_constr are equivalent if they produce the same set of new goals *)
let marked_constr_equiv_or_more_complex to_marked_constr gl c1 c2 =
  let glc1 = collect_new_goals (to_marked_constr c1) in
  let glc2 = collect_new_goals (to_marked_constr c2) in
   List.for_all (fun c -> List.exists (fun c' -> pf_conv_x gl c c') glc1) glc2

let pr_new_goals i c =
 let glc = collect_new_goals c in
  str " " ++ int i ++ str ") side conditions:" ++
   (if glc = [] then str " no side conditions"
    else
     (pr_fnl () ++ str "   " ++
       prlist_with_sep (fun () -> str "\n   ")
        (fun c -> str " ... |- " ++ pr_lconstr c) glc))

(* given a list of constr_with_marks, it returns the list where
   constr_with_marks than open more goals than simpler ones in the list
   are got rid of *)
let elim_duplicates gl to_marked_constr =
 let rec aux =
  function
     [] -> []
   | he:: tl ->
      if List.exists
          (marked_constr_equiv_or_more_complex to_marked_constr gl he) tl
      then aux tl
      else he::aux tl
 in
  aux

let filter_superset_of_new_goals gl new_goals l =
 List.filter
  (fun (_,_,c) ->
    List.for_all
     (fun g -> List.exists (pf_conv_x gl g) (collect_new_goals c)) new_goals) l

(* given the array of lists [| l1 ; ... ; ln |] it returns the list of arrays
   [ c1 ; ... ; cn ] that is the cartesian product of the sets l1, ..., ln *)
let cartesian_product gl a =
 let rec aux =
  function
     [] -> assert false
   | [he] -> List.map (fun e -> [e]) he
   | he::tl ->
      let tl' = aux tl in
       List.flatten
        (List.map (function e -> List.map (function l -> e :: l) tl') he)
 in
  List.map Array.of_list
   (aux (List.map (elim_duplicates gl identity) (Array.to_list a)))

let mark_occur gl ~new_goals t in_c input_relation input_direction =
 let rec aux output_relation output_directions in_c =
  if eq_constr t in_c then
   if List.mem input_direction output_directions
   && subrelation gl input_relation output_relation then
    [ToReplace]
   else []
  else
    match kind_of_term in_c with
      | App (c,al) -> 
         let mors_and_cs_and_als =
          let mors_and_cs_and_als =
           let morphism_table_find c =
            try morphism_table_find c with Not_found -> [] in
           let rec aux acc =
            function
               [] ->
                let c' = mkApp (c, Array.of_list acc) in
                let al' = [||] in
                List.map (fun m -> m,c',al') (morphism_table_find c')
             | (he::tl) as l ->
                let c' = mkApp (c, Array.of_list acc) in
                let al' = Array.of_list l in
                let acc' = acc @ [he] in
                 (List.map (fun m -> m,c',al') (morphism_table_find c')) @
                  (aux acc' tl)
           in
            aux [] (Array.to_list al) in
          let mors_and_cs_and_als =
           List.map
            (function (m,c,al) ->
              relation_morphism_of_constr_morphism m, c, al)
             mors_and_cs_and_als in
          let mors_and_cs_and_als =
           List.fold_left
            (fun l (m,c,al) ->
	       try (unify_morphism_with_arguments gl (c,al) m t) :: l
	       with Impossible -> l
	    ) [] mors_and_cs_and_als
          in
           List.filter
            (fun (mor,_,_) -> subrelation gl mor.output output_relation)
            mors_and_cs_and_als
         in
          (* First we look for well typed morphisms *)
          let res_mors =
           List.fold_left
            (fun res (mor,c,al) ->
              let a =
               let arguments = Array.of_list mor.args in
               let apply_variance_to_direction =
                function
                   None -> [Left2Right;Right2Left]
                 | Some true -> output_directions
                 | Some false -> List.map opposite_direction output_directions
               in
                Util.array_map2
                 (fun a (variance,relation) ->
                   (aux relation (apply_variance_to_direction variance) a)
                 ) al arguments
              in
               let a' = cartesian_product gl a in
	       List.flatten (List.map (fun output_direction ->
                (List.map
                  (function a ->
                    if not (get_mark a) then
                     ToKeep (in_c,output_relation,output_direction)
                    else
                     MApp (c,ACMorphism mor,a,output_direction)) a'))
		 output_directions) @ res
            ) [] mors_and_cs_and_als in
          (* Then we look for well typed functions *)
          let res_functions =
           (* the tactic works only if the function type is
               made of non-dependent products only. However, here we
               can cheat a bit by partially instantiating c to match
               the requirement when the arguments to be replaced are
               bound by non-dependent products only. *)
            let typeofc = Tacmach.pf_type_of gl c in
            let typ = nf_betaiota typeofc in
            let rec find_non_dependent_function env c c_args_rev typ f_args_rev
                     a_rev
            =
             function
                [] ->
                 if a_rev = [] then
		  List.map (fun output_direction ->
                   ToKeep (in_c,output_relation,output_direction))
		   output_directions
                 else
                  let a' =
                   cartesian_product gl (Array.of_list (List.rev a_rev))
                  in
                   List.fold_left
                    (fun res a ->
                      if not (get_mark a) then
			List.map (fun output_direction ->
			 (ToKeep (in_c,output_relation,output_direction)))
			 output_directions @ res
                      else
                       let err =
                        match output_relation with
                           Leibniz (Some typ') when pf_conv_x gl typ typ' ->
                            false
                         | Leibniz None -> assert false
                         | _ when output_relation = Lazy.force coq_iff_relation
                             -> false
                         | _ -> true
                       in
                        if err then res
                        else
                         let mor =
                          ACFunction{f_args=List.rev f_args_rev;f_output=typ} in
                         let func = beta_expand c c_args_rev in
			 List.map (fun output_direction ->
                          (MApp (func,mor,a,output_direction)))
			  output_directions @ res
                    ) [] a'
              | (he::tl) as a->
                 let typnf = Reduction.whd_betadeltaiota env typ in
                  match kind_of_term typnf with
                    Cast (typ,_,_) ->
                     find_non_dependent_function env c c_args_rev typ
                      f_args_rev a_rev a
                  | Prod (name,s,t) ->
                     let env' = push_rel (name,None,s) env in
                     let he =
                      (aux (Leibniz (Some s)) [Left2Right;Right2Left] he) in
                     if he = [] then []
                     else
                      let he0 = List.hd he in
                      begin
                       match noccurn 1 t, he0 with
                          _, ToKeep (arg,_,_) ->
                           (* invariant: if he0 = ToKeep (t,_,_) then every
                              element in he is = ToKeep (t,_,_) *)
                           assert
                            (List.for_all
                              (function
                                  ToKeep(arg',_,_) when pf_conv_x gl arg arg' ->
                                    true
                                | _ -> false) he) ;
                           (* generic product, to keep *)
                           find_non_dependent_function
                            env' c ((Toapply arg)::c_args_rev)
                            (subst1 arg t) f_args_rev a_rev tl
                        | true, _ ->
                           (* non-dependent product, to replace *)
                           find_non_dependent_function
                            env' c ((Toexpand (name,s))::c_args_rev)
                             (lift 1 t) (s::f_args_rev) (he::a_rev) tl
                        | false, _ ->
                           (* dependent product, to replace *)
                           (* This limitation is due to the reflexive
                             implementation and it is hard to lift *)
                           errorlabstrm "Setoid_replace"
                            (str "Cannot rewrite in the argument of a " ++
                             str "dependent product. If you need this " ++
                             str "feature, please report to the author.")
                      end
                  | _ -> assert false
            in
             find_non_dependent_function (Tacmach.pf_env gl) c [] typ [] []
              (Array.to_list al)
          in
           elim_duplicates gl identity (res_functions @ res_mors)
      | Prod (_, c1, c2) -> 
          if (dependent (mkRel 1) c2)
          then
            if (occur_term t c2)
	    then errorlabstrm "Setoid_replace"
              (str "Cannot rewrite in the type of a variable bound " ++
		  str "in a dependent product.")
	    else
	      List.map (fun output_direction ->
	       ToKeep (in_c,output_relation,output_direction)) 
	       output_directions
          else 
            let typeofc1 = Tacmach.pf_type_of gl c1 in
              if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then
		(* to avoid this error we should introduce an impl relation
                   whose first argument is Type instead of Prop. However,
                   the type of the new impl would be Type -> Prop -> Prop
                   that is no longer a Relation_Definitions.relation. Thus
                   the Coq part of the tactic should be heavily modified. *)
		errorlabstrm "Setoid_replace"
		  (str "Rewriting in a product A -> B is possible only when A " ++
		      str "is a proposition (i.e. A is of type Prop). The type " ++
		      pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++
		      str " that is not convertible to Prop.")
              else
		aux output_relation output_directions
		  (mkApp ((Lazy.force coq_impl),
			 [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |]))
      | _ ->
          if occur_term t in_c then
            errorlabstrm "Setoid_replace"
              (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++
		  str " that is not an applicative context.")
          else
	    List.map (fun output_direction ->
             ToKeep (in_c,output_relation,output_direction))
	      output_directions
 in
  let aux2 output_relation output_direction =
   List.map
    (fun res -> output_relation,output_direction,res)
     (aux output_relation [output_direction] in_c) in
  let res =
   (aux2 (Lazy.force coq_iff_relation) Right2Left) @
   (* [Left2Right] is the case of a prop of signature A ++> iff or B --> iff *)
   (aux2 (Lazy.force coq_iff_relation) Left2Right) @
   (aux2 (Lazy.force coq_impl_relation) Right2Left) in
  let res = elim_duplicates gl (function (_,_,t) -> t) res in
  let res' = filter_superset_of_new_goals gl new_goals res in
  match res' with
     [] when res = [] ->
      errorlabstrm "Setoid_rewrite"
       (str "Either the term " ++ pr_lconstr t ++ str " that must be " ++
        str "rewritten occurs in a covariant position or the goal is not " ++
        str "made of morphism applications only. You can replace only " ++
        str "occurrences that are in a contravariant position and such that " ++
        str "the context obtained by abstracting them is made of morphism " ++
        str "applications only.")
   | [] ->
      errorlabstrm "Setoid_rewrite"
       (str "No generated set of side conditions is a superset of those " ++
        str "requested by the user. The generated sets of side conditions " ++
        str "are: " ++
         pr_fnl () ++
         prlist_with_sepi pr_fnl
          (fun i (_,_,mc) -> pr_new_goals i mc) res)
   | [he] -> he
   | he::_ ->
      ppnl
       (str "Warning: The application of the tactic is subject to one of " ++
        str "the \nfollowing set of side conditions that the user needs " ++
        str "to prove:" ++
         pr_fnl () ++
         prlist_with_sepi pr_fnl
          (fun i (_,_,mc) -> pr_new_goals i mc) res' ++ pr_fnl () ++
         str "The first set is randomly chosen. Use the syntax " ++
         str "\"setoid_rewrite ... generate side conditions ...\" to choose " ++
         str "a different set.") ;
      he

let cic_morphism_context_list_of_list hole_relation hole_direction out_direction
=
 let check =
  function
     (None,dir,dir') -> 
      mkApp ((Lazy.force coq_MSNone), [| dir ; dir' |])
   | (Some true,dir,dir') ->
      assert (dir = dir');
      mkApp ((Lazy.force coq_MSCovariant), [| dir |])
   | (Some false,dir,dir') ->
      assert (dir <> dir');
      mkApp ((Lazy.force coq_MSContravariant), [| dir |]) in
 let rec aux =
  function
     [] -> assert false
   | [(variance,out),(value,direction)] ->
      mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class ; out |]),
      mkApp ((Lazy.force coq_fcl_singl),
       [| hole_relation; hole_direction ; out ;
          direction ; out_direction ;
          check (variance,direction,out_direction) ; value |])
   | ((variance,out),(value,direction))::tl ->
      let outtl, valuetl = aux tl in
       mkApp ((Lazy.force coq_cons),
        [| Lazy.force coq_Argument_Class ; out ; outtl |]),
       mkApp ((Lazy.force coq_fcl_cons),
        [| hole_relation ; hole_direction ; out ; outtl ;
           direction ; out_direction ;
           check (variance,direction,out_direction) ;
           value ; valuetl |])
 in aux

let rec cic_type_nelist_of_list =
 function
    [] -> assert false
  | [value] ->
      mkApp ((Lazy.force coq_singl), [| mkType (Termops.new_univ ()) ; value |])
  | value::tl ->
     mkApp ((Lazy.force coq_cons),
      [| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |])

let syntactic_but_representation_of_marked_but hole_relation hole_direction =
 let rec aux out (rel_out,precise_out,is_reflexive) =
  function
     MApp (f, m, args, direction) ->
      let direction = cic_direction_of_direction direction in
      let morphism_theory, relations =
       match m with
          ACMorphism { args = args ; morphism_theory = morphism_theory } ->
           morphism_theory,args
        | ACFunction { f_args = f_args ; f_output = f_output } ->
           let mt =
            if eq_constr out (cic_relation_class_of_relation_class
              (Lazy.force coq_iff_relation))
            then
              mkApp ((Lazy.force coq_morphism_theory_of_predicate),
               [| cic_type_nelist_of_list f_args; f|])
            else
              mkApp ((Lazy.force coq_morphism_theory_of_function),
               [| cic_type_nelist_of_list f_args; f_output; f|])
           in
            mt,List.map (fun x -> None,Leibniz (Some x)) f_args in
      let cic_relations =
       List.map
        (fun (variance,r) ->
          variance,
          r,
          cic_relation_class_of_relation_class r,
          cic_precise_relation_class_of_relation_class r
        ) relations in
      let cic_args_relations,argst =
       cic_morphism_context_list_of_list hole_relation hole_direction direction
        (List.map2
         (fun (variance,trel,t,precise_t) v ->
           (variance,cic_argument_class_of_argument_class (variance,trel)),
             (aux t precise_t v,
               direction_of_constr_with_marks hole_direction v)
         ) cic_relations (Array.to_list args))
      in
       mkApp ((Lazy.force coq_App),
        [|hole_relation ; hole_direction ;
          cic_args_relations ; out ; direction ;
          morphism_theory ; argst|])
   | ToReplace ->
      mkApp ((Lazy.force coq_ToReplace), [| hole_relation ; hole_direction |])
   | ToKeep (c,_,direction) ->
      let direction = cic_direction_of_direction direction in
       if is_reflexive then
        mkApp ((Lazy.force coq_ToKeep),
         [| hole_relation ; hole_direction ; precise_out ; direction ; c |])
       else
        let c_is_proper =
         let typ = mkApp (rel_out, [| c ; c |]) in
          mkCast (Evarutil.mk_new_meta (),DEFAULTcast, typ)
        in
         mkApp ((Lazy.force coq_ProperElementToKeep),
          [| hole_relation ; hole_direction; precise_out ;
             direction; c ; c_is_proper |])
 in aux

let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h)
 prop_direction m
=
 let hole_relation = cic_relation_class_of_relation_class hole_relation in
 let hyp,hole_direction = h,cic_direction_of_direction direction in
 let cic_prop_relation = cic_relation_class_of_relation_class prop_relation in
 let precise_prop_relation =
  cic_precise_relation_class_of_relation_class prop_relation
 in
  mkApp ((Lazy.force coq_setoid_rewrite),
   [| hole_relation ; hole_direction ; cic_prop_relation ;
      prop_direction ; c1 ; c2 ;
      syntactic_but_representation_of_marked_but hole_relation hole_direction
       cic_prop_relation precise_prop_relation m ; hyp |])

let check_evar_map_of_evars_defs evd =
 let metas = Evd.meta_list evd in
 let check_freemetas_is_empty rebus =
  Evd.Metaset.iter
   (fun m ->
     if Evd.meta_defined evd m then () else
      raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
 in
  List.iter
   (fun (_,binding) ->
     match binding with
        Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
         check_freemetas_is_empty rebus freemetas
      | Evd.Clval (_,{Evd.rebus=rebus1; Evd.freemetas=freemetas1},
                 {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
         check_freemetas_is_empty rebus1 freemetas1 ;
         check_freemetas_is_empty rebus2 freemetas2
   ) metas

(* For a correct meta-aware "rewrite in", we split unification 
   apart from the actual rewriting (Pierre L, 05/04/06) *)
   
(* [unification_rewrite] searchs a match for [c1] in [but] and then 
   returns the modified objects (in particular [c1] and [c2]) *)  

let unification_rewrite c1 c2 cl but gl = 
  let (env',c1) =
    try
      (* ~mod_delta:false to allow to mark occurences that must not be
         rewritten simply by replacing them with let-defined definitions
         in the context *)
      w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env
    with
	Pretype_errors.PretypeError _ ->
	  (* ~mod_delta:true to make Ring work (since it really
             exploits conversion) *)
	  w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env
  in
  let cl' = {cl with env = env' } in
  let c2 = Clenv.clenv_nf_meta cl' c2 in
  check_evar_map_of_evars_defs env' ;
  env',Clenv.clenv_value cl', c1, c2

(* no unification is performed in this function. [sigma] is the 
 substitution obtained from an earlier unification. *)

let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl = 
  let but = pf_concl gl in 
  try
   let input_relation =
    relation_class_that_matches_a_constr "Setoid_rewrite"
     new_goals (Typing.mtype_of (pf_env gl) sigma (snd hyp)) in
   let output_relation,output_direction,marked_but =
    mark_occur gl ~new_goals c1 but input_relation (fst hyp) in
   let cic_output_direction = cic_direction_of_direction output_direction in
   let if_output_relation_is_iff gl =
    let th =
     apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
      cic_output_direction marked_but
    in
     let new_but = Termops.replace_term c1 c2 but in
     let hyp1,hyp2,proj =
      match output_direction with
         Right2Left -> new_but, but, Lazy.force coq_proj1
       | Left2Right -> but, new_but, Lazy.force coq_proj2
     in
     let impl1 = mkProd (Anonymous, hyp2, lift 1 hyp1) in
     let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
      let th' = mkApp (proj, [|impl2; impl1; th|]) in
       Tactics.refine
        (mkApp (th',[|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
	gl in
   let if_output_relation_is_if gl =
    let th =
     apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
      cic_output_direction marked_but
    in
     let new_but = Termops.replace_term c1 c2 but in
      Tactics.refine
       (mkApp (th, [|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
       gl in
   if output_relation = (Lazy.force coq_iff_relation) then
     if_output_relation_is_iff gl
   else
     if_output_relation_is_if gl
  with
    Optimize ->
      !general_rewrite (fst hyp = Left2Right) (snd hyp) gl

let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
 let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl (pf_concl gl) gl in 
 relation_rewrite_no_unif c1 c2 (input_direction,cl) ~new_goals sigma gl 

let analyse_hypothesis gl c =
 let ctype = pf_type_of gl c in
 let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
 let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
 let rec split_last_two = function
   | [c1;c2] -> [],(c1, c2)
   | x::y::z ->
      let l,res = split_last_two (y::z) in x::l, res
   | _ -> error "The term provided is not an equivalence" in
 let others,(c1,c2) = split_last_two args in
  eqclause,mkApp (equiv, Array.of_list others),c1,c2

let general_s_rewrite lft2rgt c ~new_goals gl =
  let eqclause,_,c1,c2 = analyse_hypothesis gl c in
  if lft2rgt then 
    relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl
  else 
    relation_rewrite c2 c1 (Right2Left,eqclause) ~new_goals gl

let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl = 
 let hyp = pf_type_of gl (mkVar id) in
 (* first, we find a match for c1 in the hyp *)
 let (sigma,cl,c1,c2) = unification_rewrite c1 c2 eqclause hyp gl in 
 (* since we will actually rewrite in the opposite direction, we also need
    to replace every occurrence of c2 (resp. c1) in hyp with something that
    is convertible but not syntactically equal. To this aim we introduce a
    let-in and then we will use the intro tactic to get rid of it.
    Quite tricky to do properly since c1 can occur in c2 or vice-versa ! *)
 let mangled_new_hyp = 
   let hyp = lift 2 hyp in 
   (* first, we backup every occurences of c1 in newly allocated (Rel 1) *)
   let hyp = Termops.replace_term (lift 2 c1) (mkRel 1) hyp in 
   (* then, we factorize every occurences of c2 into (Rel 2) *)
   let hyp = Termops.replace_term (lift 2 c2) (mkRel 2) hyp in 
   (* Now we substitute (Rel 1) (i.e. c1) for c2 *)
   let hyp = subst1 (lift 1 c2) hyp in 
   (* Since subst1 has killed Rel 1 and decreased the other Rels, 
      Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
   mkLetIn (Anonymous,c2,pf_type_of gl c2,hyp) 
 in 
 let new_hyp = Termops.replace_term c1 c2 hyp in 
 let oppdir = opposite_direction direction in 
 cut_replacing id new_hyp
   (tclTHENLAST
      (tclTHEN (change_in_concl None mangled_new_hyp)
         (tclTHEN intro
            (relation_rewrite_no_unif c2 c1 (oppdir,cl) ~new_goals sigma))))
   gl

let general_s_rewrite_in id lft2rgt c ~new_goals gl =
  let eqclause,_,c1,c2 = analyse_hypothesis gl c in
  if lft2rgt then 
    relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl
  else 
    relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl


(* 
   [general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals ]
   common part of [setoid_replace] and [setoid_replace_in]  (distinction is done using rewrite_tac). 

   Algorith sketch: 
   1- find the (setoid) relation [rel] between [c1] and [c2] using [relation]
   2- assert [H:rel c2 c1] 
   3- replace [c1] with [c2] using [rewrite_tac] (should be [general_s_rewrite] if we want to replace in the 
      goal, and [general_s_rewrite_in id] if we want to replace in the hypothesis [id]). Possibly generate
      new_goals if asked (cf general_s_rewrite)
   4- if [try_prove_eq_tac_opt] is [Some tac] try to complete [rel c2 c1] using tac and do nothing if 
      [try_prove_eq_tac_opt] is [None]
*)
let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals gl =
  let try_prove_eq_tac = 
    match try_prove_eq_tac_opt with 
      | None -> Tacticals.tclIDTAC
      | Some tac ->  Tacticals.tclTRY (Tacticals.tclCOMPLETE tac )
  in 
  try
    let carrier,args = decompose_app (pf_type_of gl c1) in
    let relation =
      match relation with
	  Some rel ->
	    (try
		match find_relation_class rel with
		    Relation sa -> if not (eq_constr carrier sa.rel_a) then 		    
			errorlabstrm "Setoid_rewrite"
			  (str "the carrier of " ++ pr_lconstr rel ++ 
			      str " does not match the type of " ++ pr_lconstr c1);
		      sa
		  | Leibniz _ -> raise Optimize
              with
		  Not_found ->
		    errorlabstrm "Setoid_rewrite"
		      (pr_lconstr rel ++ str " is not a registered relation."))
	| None ->
	    match default_relation_for_carrier (pf_type_of gl c1) with
		Relation sa -> sa
              | Leibniz _ -> raise Optimize
    in
    let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in
    let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in
    let replace dir eq =
      tclTHENS (assert_tac false Anonymous eq)
	[onLastHyp (fun id ->
          tclTHEN
            (rewrite_tac dir (mkVar id) ~new_goals)
            (clear [id]));
	 try_prove_eq_tac]
    in
      tclORELSE
	(replace true eq_left_to_right) (replace false eq_right_to_left) gl
  with
      Optimize -> (* (!replace tac_opt c1 c2) gl *)
	let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
	  tclTHENS (assert_tac false Anonymous eq)
	    [onLastHyp (fun id ->
	      tclTHEN
		(rewrite_tac false (mkVar id) ~new_goals)
		(clear [id]));
	     try_prove_eq_tac] gl
      
let setoid_replace = general_setoid_replace general_s_rewrite
let setoid_replace_in  tac_opt id relation c1 c2 ~new_goals gl = 
  general_setoid_replace (general_s_rewrite_in id)  tac_opt relation c1 c2 ~new_goals gl
 
(* [setoid_]{reflexivity,symmetry,transitivity} tactics *)

let setoid_reflexivity gl =
 try
  let relation_class =
   relation_class_that_matches_a_constr "Setoid_reflexivity"
    [] (pf_concl gl) in
  match relation_class with
     Leibniz _ -> assert false (* since [] is empty *)
   | Relation rel ->
      match rel.rel_refl with
         None ->
          errorlabstrm "Setoid_reflexivity"
           (str "The relation " ++ prrelation rel ++ str " is not reflexive.")
       | Some refl -> apply refl gl
 with
  Optimize -> reflexivity_red true gl

let setoid_symmetry gl =
 try
  let relation_class =
   relation_class_that_matches_a_constr "Setoid_symmetry"
    [] (pf_concl gl) in
  match relation_class with
     Leibniz _ -> assert false (* since [] is empty *)
   | Relation rel ->
      match rel.rel_sym with
         None ->
          errorlabstrm "Setoid_symmetry"
           (str "The relation " ++ prrelation rel ++ str " is not symmetric.")
       | Some sym -> apply sym gl
 with
  Optimize -> symmetry_red true gl

let setoid_symmetry_in id gl =
  let ctype = pf_type_of gl (mkVar id) in
  let binders,concl = Sign.decompose_prod_assum ctype in
  let (equiv, args) = decompose_app concl in
  let rec split_last_two = function
    | [c1;c2] -> [],(c1, c2)
    | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
    | _ -> error "The term provided is not an equivalence" 
  in
  let others,(c1,c2) = split_last_two args in
  let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
  let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
  let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
  tclTHENS (cut new_hyp)
    [ intro_replacing id;
      tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ]
    gl

let setoid_transitivity c gl =
 try
  let relation_class =
   relation_class_that_matches_a_constr "Setoid_transitivity"
    [] (pf_concl gl) in
  match relation_class with
     Leibniz _ -> assert false (* since [] is empty *)
   | Relation rel ->
      let ctyp = pf_type_of gl c in
      let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in
       match rel'.rel_trans with
          None ->
           errorlabstrm "Setoid_transitivity"
            (str "The relation " ++ prrelation rel ++ str " is not transitive.")
        | Some trans ->
           let transty = nf_betaiota (pf_type_of gl trans) in
           let argsrev, _ =
            Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in
           let binder =
            match List.rev argsrev with
               _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2
             | _ -> assert false
           in
            apply_with_bindings
             (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
 with
  Optimize -> transitivity_red true c gl
;;

Tactics.register_setoid_reflexivity setoid_reflexivity;;
Tactics.register_setoid_symmetry setoid_symmetry;;
Tactics.register_setoid_symmetry_in setoid_symmetry_in;;
Tactics.register_setoid_transitivity setoid_transitivity;;