Inference Rules: Revision history

3 June 2024

• curprev 15:1015:10, 3 June 2024‎ Guillaume talk contribs‎ 36,436 bytes +1‎ Rule FIN_COMPSET_R has been implemented in Rodin 3.9

1 February 2024

• curprev 10:2210:22, 1 February 2024‎ Guillaume talk contribs‎ 36,435 bytes +203‎ Add rule for finiteness of explicit set comprehension

13 April 2023

• curprev 14:3214:32, 13 April 2023‎ Guillaume talk contribs‎ 36,232 bytes +2‎ Rules EQV_LR and EQV_RL were implemented

6 April 2023

• curprev 09:3009:30, 6 April 2023‎ Guillaume talk contribs‎ 36,230 bytes 0‎ Add star to proof rules implemented in Rodin 3.8

21 October 2022

• curprev 15:2615:26, 21 October 2022‎ Guillaume talk contribs‎ 36,230 bytes +26‎ Fix inference rule FIN_KUNION_R

17 October 2022

• curprev 09:2009:20, 17 October 2022‎ Guillaume talk contribs‎ 36,204 bytes +694‎ Add rules for finiteness of union

23 June 2014

• curprev 16:0016:00, 23 June 2014‎ imported>Nicolas‎ m 35,510 bytes −595‎ Removed induction on integers (was wrong), reviewed induciton on naturals
• curprev 13:4713:47, 23 June 2014‎ imported>Nicolas‎ m 36,105 bytes +1,449‎ Added INDUC_* inference rules

13 June 2014

• curprev 14:2414:24, 13 June 2014‎ imported>Laurent‎ 34,656 bytes +218‎ Split EQV into EQV_LR and EQV_RL

29 August 2013

• curprev 10:1410:14, 29 August 2013‎ imported>Laurent‎ m 34,438 bytes +2‎ No edit summary

20 August 2013

• curprev 12:1412:14, 20 August 2013‎ imported>Josselin‎ 34,436 bytes +266‎ Add scalar case in Variants array.

1 August 2013

• curprev 15:4215:42, 1 August 2013‎ imported>Josselin‎ 34,170 bytes +679‎ added space in array for improved readability
• curprev 13:4113:41, 1 August 2013‎ imported>Josselin‎ 33,491 bytes +1,252‎ Fix HYP, HYPOR, GenMP rules + added inclusion cases

31 July 2013

• curprev 09:3909:39, 31 July 2013‎ imported>Josselin‎ 32,239 bytes −301‎ moved explanation in Variants_in_HYP,_CNTR_and_GenMP page

30 July 2013

• curprev 16:0116:01, 30 July 2013‎ imported>Josselin‎ 32,540 bytes 0‎ Fix explanation about variants of P and not P
• curprev 14:3314:33, 30 July 2013‎ imported>Josselin‎ 32,540 bytes +55‎ Added new variants of P and not P

30 May 2013

• curprev 08:4908:49, 30 May 2013‎ imported>Josselin‎ 32,485 bytes −112‎ Fix HYP rule (Removed predicate with a not symbol)

28 May 2013

• curprev 11:0611:06, 28 May 2013‎ imported>Josselin‎ 32,597 bytes +2‎ Fix rule CNTR
• curprev 10:0510:05, 28 May 2013‎ imported>Josselin‎ 32,595 bytes +290‎ Fix GENMP rules
• curprev 08:3508:35, 28 May 2013‎ imported>Josselin‎ 32,305 bytes −119‎ Remove 2 rows from the new array
• curprev 08:3108:31, 28 May 2013‎ imported>Josselin‎ 32,424 bytes +172‎ Fix rules HYP_OR, GENMP_OR_GOAL_HYP, GENMP_OR_NOT_GOAL_HYP
• curprev 08:2208:22, 28 May 2013‎ imported>Josselin‎ 32,252 bytes +48‎ Add side condition (CNTR rule)

27 May 2013

• curprev 15:4615:46, 27 May 2013‎ imported>Josselin‎ 32,204 bytes +1,857‎ Fix rules HYP and CNTR (case distinction on relational predicate)

10 September 2012

• curprev 09:5809:58, 10 September 2012‎ imported>Billaude‎ m 30,347 bytes +8‎ SIM_OV_REL, SIM_OV_TREL, SIM_OV_PFUN and SIM_OV_TFUN were miswritten.

29 September 2011

• curprev 14:5414:54, 29 September 2011‎ imported>Billaude‎ 30,339 bytes +110‎ Add a missing rule. Correct two rule's names.

28 September 2011

• curprev 16:3416:34, 28 September 2011‎ imported>Billaude‎ 30,229 bytes +4,431‎ Add inference rules used in MapOvrGoal, MembershipGoal (so far), GeneralizedModusPonens and the AutoRewriterL3.

23 August 2011

• curprev 11:1611:16, 23 August 2011‎ imported>Billaude‎ 25,798 bytes −320‎ No edit summary

23 May 2011

• curprev 07:2507:25, 23 May 2011‎ imported>Billaude‎ m 26,118 bytes 0‎ IMP_CASE is now marked as implemented.

5 April 2011

• curprev 09:2009:20, 5 April 2011‎ imported>Laurent‎ m 26,118 bytes 0‎ No edit summary

4 April 2011

• curprev 16:4416:44, 4 April 2011‎ imported>Laurent‎ 26,118 bytes +821‎ Added rules FIN_REL, FIN_FUN_DOM and FIN_FUN_RAN
• curprev 15:0315:03, 4 April 2011‎ imported>Laurent‎ 25,297 bytes +268‎ Added rule IMP_CASE

30 March 2011

• curprev 14:5214:52, 30 March 2011‎ imported>Nicolas‎ m 25,029 bytes 0‎ NEG_IN_L and NEG_IN_R back to implemented status, after checking implementation
• curprev 14:3114:31, 30 March 2011‎ imported>Laurent‎ 25,029 bytes +32‎ FIxed rules NEG_IN_L and NEG_IN_R (see bug #3244113).

8 February 2011

• curprev 14:4114:41, 8 February 2011‎ imported>Tommy‎ m 24,997 bytes +1‎ Implemented FORALL_INST_MT in r10767.

7 February 2011

• curprev 13:4513:45, 7 February 2011‎ imported>Tommy‎ m 24,996 bytes +427‎ Added FORALL_INST_MT rule

14 December 2010

• curprev 12:5612:56, 14 December 2010‎ imported>Laurent‎ m 24,569 bytes −1‎ No edit summary
• curprev 12:5512:55, 14 December 2010‎ imported>Laurent‎ 24,570 bytes +237‎ Fixed FIN_QINTER_R and added FIN_KINTER_R

13 December 2010

• curprev 17:0417:04, 13 December 2010‎ imported>Nicolas‎ 24,333 bytes +195‎ added rule FIN_QINTER_R

16 November 2010

• curprev 13:4713:47, 16 November 2010‎ imported>Laurent‎ m 24,138 bytes 0‎ Marked rules ONE_POINT_L and ONE_POINT_R as implemented
• curprev 13:3413:34, 16 November 2010‎ imported>Laurent‎ m 24,138 bytes 0‎ Marked rule FUN_IMAGE_GOAL as implemented

15 October 2010

• curprev 08:2608:26, 15 October 2010‎ imported>Desaperh‎ 24,138 bytes 0‎ No edit summary

8 October 2010

• curprev 14:5614:56, 8 October 2010‎ imported>Desaperh‎ 24,138 bytes 0‎ Rule FUN_IMAGE_GOAL has been implemented

17 September 2010

• curprev 16:4716:47, 17 September 2010‎ imported>Laurent‎ 24,138 bytes −172‎ Removed WD-strictness condition where it was unnecessary and unimplemented.
• curprev 14:3214:32, 17 September 2010‎ imported>Laurent‎ 24,310 bytes −321‎ Replaced "top-level" with WD strictness or freeness condition.

9 September 2010

• curprev 12:2712:27, 9 September 2010‎ imported>Nicolas‎ m 24,631 bytes −1,120‎ moved datatype rules to extension proof rules page

6 September 2010

• curprev 08:5408:54, 6 September 2010‎ imported>Nicolas‎ m 25,751 bytes +34‎ added a link to datatype rule examples
• curprev 08:2508:25, 6 September 2010‎ imported>Nicolas‎ m 25,717 bytes −71‎ simplified representation of rule DATATYPE_INDUCTION (the meaning remains the same)

30 August 2010

• curprev 12:1412:14, 30 August 2010‎ imported>Wohuai‎ m 25,788 bytes +191‎ No edit summary

27 August 2010

• curprev 14:0814:08, 27 August 2010‎ imported>Laurent‎ 25,597 bytes 0‎ Rule FUN_IMAGE_GOAL is manual
• curprev 13:1313:13, 27 August 2010‎ imported>Laurent‎ 25,597 bytes +348‎ Added rule FUN_IMAGE_GOAL

25 August 2010

• curprev 16:5616:56, 25 August 2010‎ imported>Laurent‎ 25,249 bytes −238‎ Changed REC_FUN_GOAL to FUN_GOAL_REC and fixed typing.

23 August 2010

• curprev 13:1413:14, 23 August 2010‎ imported>Desaperh‎ 25,487 bytes +760‎ Added rule REC_FUN_GOAL
• curprev 13:1213:12, 23 August 2010‎ imported>Desaperh‎ 24,727 bytes −760‎ Undo revision 6711 by Desaperh (Talk)
• curprev 13:0913:09, 23 August 2010‎ imported>Desaperh‎ 25,487 bytes +760‎ No edit summary

6 August 2010

• curprev 13:5513:55, 6 August 2010‎ imported>Nicolas‎ 24,727 bytes +584‎ added DATATYPE_INDUCTION; rewrote DATATYPE_DISTINCT_CASE
• curprev 12:3812:38, 6 August 2010‎ imported>Nicolas‎ 24,143 bytes +625‎ added DATATYPE_DISTINCT_CASE

4 August 2010

• curprev 16:3716:37, 4 August 2010‎ imported>Pascal‎ 23,518 bytes +129‎ No edit summary

28 April 2010

• curprev 13:4713:47, 28 April 2010‎ imported>Tommy‎ 23,389 bytes −884‎ Rules OV_SETENUM_L (resp. OV_SETENUM_R) and OV_L (resp. OV_R) have been implemented in r8699.

21 April 2010

• curprev 16:4616:46, 21 April 2010‎ imported>Tommy‎ 24,273 bytes +13‎ Added rules FUNIMG_SET_DOMSUB_L and FUNIMG_DOMSUB_L
• curprev 16:3216:32, 21 April 2010‎ imported>Tommy‎ m 24,260 bytes +871‎ No edit summary
• curprev 15:2715:27, 21 April 2010‎ imported>Laurent‎ 23,389 bytes +6‎ Fixed rules OV_L, OV_R, OV_SETENUM_L, and OV_SETENUM_R.
• curprev 15:2015:20, 21 April 2010‎ imported>Tommy‎ m 23,383 bytes +80‎ No edit summary
• curprev 13:0613:06, 21 April 2010‎ imported>Tommy‎ m 23,303 bytes 0‎ No edit summary

27 March 2010

• curprev 22:3022:30, 27 March 2010‎ imported>Laurent‎ m 23,303 bytes +8‎ No edit summary

1 February 2010

• curprev 11:5611:56, 1 February 2010‎ imported>Laurent‎ 23,295 bytes +1,470‎ Added rules SIMP_CARD_SETMINUS_L, SIMP_CARD_SETMINUS_R, SIMP_CARD_CPROD_L and SIMP_CARD_CPROD_R (were previously rewrite rules).

15 January 2010

• curprev 11:0711:07, 15 January 2010‎ imported>Laurent‎ 21,825 bytes 0‎ Marked CARD_EMPTY_INTERV as not implemented.
• curprev 09:5009:50, 15 January 2010‎ imported>Laurent‎ 21,825 bytes 0‎ Implementation of rule EXISTS_INST has been confirmed correct

13 January 2010

• curprev 15:4315:43, 13 January 2010‎ imported>Tommy‎ m 21,825 bytes 0‎ Mark FIN_FUN_* as fixed(*). Fixed in r8042.

7 January 2010

• curprev 11:0811:08, 7 January 2010‎ imported>Laurent‎ 21,825 bytes +813‎ Replaced CARD_SUBSETEQ by DERIV_LE_CARD, DERIV_GE_CARD, DERIV_LT_CARD, DERIV_GT_CARD, DERIV_EQUAL_CARD.

23 December 2009

• curprev 11:5311:53, 23 December 2009‎ imported>Laurent‎ 21,012 bytes 0‎ Code for rules FIN_SUBSETEQ_R and FIN_REL_R is now fixed in Subversion.

21 December 2009

• curprev 09:2509:25, 21 December 2009‎ imported>Tommy‎ m 21,012 bytes −3‎ removed * on unimplemented rules

14 November 2009

• curprev 14:4714:47, 14 November 2009‎ imported>Laurent‎ m 21,015 bytes 0‎ Rules MH and HM have been fixed

11 November 2009

• curprev 18:0118:01, 11 November 2009‎ imported>Laurent‎ 21,015 bytes −32‎ Fixed EXISTS_INST which was on the wrong side.
• curprev 17:5617:56, 11 November 2009‎ imported>Laurent‎ m 21,047 bytes −354‎ Fixed silly side conditions
• curprev 17:4617:46, 11 November 2009‎ imported>Laurent‎ m 21,401 bytes −32‎ Fixed more spacing in formulas
• curprev 17:4017:40, 11 November 2009‎ imported>Laurent‎ m 21,433 bytes −293‎ FIxed spacing in formulas
• curprev 11:0711:07, 11 November 2009‎ imported>Laurent‎ 21,726 bytes +535‎ Fixed broken rules (ill-defined, ill-typed or plain wrong)

8 October 2009

• curprev 16:0816:08, 8 October 2009‎ imported>Nicolas‎ m 21,191 bytes −24‎ Undo revision 4260 by Nicolas (Talk)
• curprev 13:1813:18, 8 October 2009‎ imported>Nicolas‎ m 21,215 bytes +24‎ corrected FORALL_INST_MP: added [x:=E] P hypothesis to 3rd antecedent (similar to MH)

18 August 2009

• curprev 09:0409:04, 18 August 2009‎ imported>Nicolas‎ m 21,191 bytes +288‎ added SIM_REL_IMAGE_L (for implementation traceability purposes)
• curprev 08:5808:58, 18 August 2009‎ imported>Nicolas‎ m 20,903 bytes +301‎ added SIM_FCOMP_L (for implementation traceability purposes)
• curprev 08:5408:54, 18 August 2009‎ imported>Nicolas‎ m 20,602 bytes +369‎ added DIS_SETMINUS_L (for implementation traceability purposes)

17 August 2009

• curprev 14:0514:05, 17 August 2009‎ imported>Nicolas‎ m 20,233 bytes +840‎ added FIN_L_* rules
• curprev 13:2013:20, 17 August 2009‎ imported>Nicolas‎ m 19,393 bytes +362‎ added DIS_BINTER_L

15 July 2009

• curprev 09:0009:00, 15 July 2009‎ imported>Nicolas‎ m 19,031 bytes +172‎ Added comment for one point rule with 'exists' quantifier

10 July 2009

• curprev 14:5214:52, 10 July 2009‎ imported>Nicolas‎ m 18,859 bytes +886‎ added ONE_POINT_L

8 July 2009

• curprev 10:2510:25, 8 July 2009‎ imported>Laurent‎ m 17,973 bytes −756‎ Fixed rule names to make them easy to extract
• curprev 09:3609:36, 8 July 2009‎ imported>Laurent‎ 18,729 bytes +259‎ Added AUTO_MH

6 July 2009

• curprev 13:2813:28, 6 July 2009‎ imported>Laurent‎ m 18,470 bytes +18‎ No edit summary
• curprev 13:2113:21, 6 July 2009‎ imported>Laurent‎ m 18,452 bytes +1‎ Renamed SIM_FUN into FUN_GOAL.
• curprev 13:1813:18, 6 July 2009‎ imported>Laurent‎ m 18,451 bytes −5‎ No edit summary
• curprev 13:1813:18, 6 July 2009‎ imported>Laurent‎ 18,456 bytes +386‎ Added SIM_FUN
• curprev 10:1510:15, 6 July 2009‎ imported>Laurent‎ m 18,070 bytes −15‎ Fixed DIS_SETMINUS_R

3 July 2009

• curprev 14:4814:48, 3 July 2009‎ imported>Nicolas‎ m 18,085 bytes +386‎ added DISTINCT_CASE
• curprev 14:2614:26, 3 July 2009‎ imported>Nicolas‎ m 17,699 bytes +304‎ added EXISTS_INST
• curprev 14:2214:22, 3 July 2009‎ imported>Nicolas‎ m 17,395 bytes +30‎ added H as hyposthesis for WD in FORALL_INST, FORALL_INST_MP, CUT
• curprev 14:2014:20, 3 July 2009‎ imported>Nicolas‎ m 17,365 bytes −37‎ removed bold font in WD ;; used correct symbol for :=
• curprev 14:0914:09, 3 July 2009‎ imported>Nicolas‎ m 17,402 bytes +359‎ added CUT
• curprev 13:5013:50, 3 July 2009‎ imported>Nicolas‎ m 17,043 bytes +482‎ added FORALL_INST_MP
• curprev 13:3813:38, 3 July 2009‎ imported>Nicolas‎ m 16,561 bytes +247‎ added FORALL_INST