Extension Proof Rules - Revision history

imported>WikiSysop: /* Rewrite Rules */

2019-11-29T15:38:43Z

Rewrite Rules

← Older revision		Revision as of 15:38, 29 November 2019
Line 6:		Line 6:

	{{RRHeader}}		{{RRHeader}}
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| AA		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_COND}}\|\|<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_COND}}\|\|<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>\|\| \|\| A

imported>WikiSysop: /* Rewrite Rules */

2019-11-29T15:38:35Z

Rewrite Rules

← Older revision		Revision as of 15:38, 29 November 2019
Line 6:		Line 6:

	{{RRHeader}}		{{RRHeader}}
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| AA
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_COND}}\|\|<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_COND}}\|\|<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>\|\| \|\| A
	\|}		\|}


	=== Inference Rules ===		=== Inference Rules ===

imported>Nicolas: /* Inference Rules */

2010-11-16T13:04:10Z

Inference Rules

← Older revision		Revision as of 13:04, 16 November 2010
Line 14:		Line 14:
	=== Inference Rules ===		=== Inference Rules ===
	{{RRHeader}}		{{RRHeader}}
	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M

	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_INDUCTION}}\|\|<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>\|\| where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples [[Datatype Rules\|here]] \|\| M		{{RRRow}}\|*\|\|{{Rulename\|DATATYPE_INDUCTION}}\|\|<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>\|\| where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples [[Datatype Rules\|here]] \|\| M
	\|}		\|}

imported>Laurent at 11:07, 10 November 2010

2010-11-10T11:07:44Z

← Older revision		Revision as of 11:07, 10 November 2010
Line 3:		Line 3:
	Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].		Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].

	== Rewrite Rules ==		=== Rewrite Rules ===

	{{RRHeader}}		{{RRHeader}}
Line 12:		Line 12:


	== Inference Rules ==		=== Inference Rules ===
	{{RRHeader}}		{{RRHeader}}
	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M		{{RRRow}}\| \|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M

imported>Nicolas: SIMP_MULTI_COND was implemented

2010-09-13T17:24:06Z

SIMP_MULTI_COND was implemented

← Older revision		Revision as of 17:24, 13 September 2010
Line 8:		Line 8:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_MULTI_COND}}\|\|<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_MULTI_COND}}\|\|<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>\|\| \|\| A
	\|}		\|}

imported>Nicolas at 12:52, 10 September 2010

2010-09-10T12:52:32Z

← Older revision		Revision as of 12:52, 10 September 2010
Line 8:		Line 8:
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A
	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A
			{{RRRow}}\| \|\|{{Rulename\|SIMP_MULTI_COND}}\|\|<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>\|\| \|\| A
	\|}		\|}

imported>Nicolas: copied datatype inference rules

2010-09-09T12:24:56Z

copied datatype inference rules

← Older revision		Revision as of 12:24, 9 September 2010
Line 13:		Line 13:
	== Inference Rules ==		== Inference Rules ==
	{{RRHeader}}		{{RRHeader}}
			{{RRRow}}\| \|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M

			{{RRRow}}\| \|\|{{Rulename\|DATATYPE_INDUCTION}}\|\|<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>\|\| where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples [[Datatype Rules\|here]] \|\| M
	\|}		\|}

imported>Nicolas at 10:27, 9 September 2010

2010-09-09T10:27:08Z

← Older revision		Revision as of 10:27, 9 September 2010
Line 2:		Line 2:
	Rules without a <tt>*</tt> are planned to be implemented in future versions.		Rules without a <tt>*</tt> are planned to be implemented in future versions.
	Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].		Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].

			== Rewrite Rules ==

	{{RRHeader}}		{{RRHeader}}
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A
	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A		{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A
	\|}		\|}


			== Inference Rules ==
			{{RRHeader}}

			\|}

	[[Category:User documentation\|The Proving Perspective]]		[[Category:User documentation\|The Proving Perspective]]
	[[Category:Rodin Platform\|The Proving Perspective]]		[[Category:Rodin Platform\|The Proving Perspective]]
	[[Category:User manual\|The Proving Perspective]]		[[Category:User manual\|The Proving Perspective]]

imported>Nicolas: Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page.

2010-09-09T10:23:50Z

Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page.

← Older revision	Revision as of 10:23, 9 September 2010
(No difference)

imported>Nicolas: added rules SIMP_SPECIAL_COND_BTRUE and SIMP_SPECIAL_COND_BFALSE

2010-09-03T17:15:05Z

added rules SIMP_SPECIAL_COND_BTRUE and SIMP_SPECIAL_COND_BFALSE

New page

Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
Rules without a <tt>*</tt> are planned to be implemented in future versions.
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].

{{RRHeader}}
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COND_BTRUE}}||<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>|| || A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COND_BFALSE}}||<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>|| || A
|}

[[Category:User documentation|The Proving Perspective]]
[[Category:Rodin Platform|The Proving Perspective]]
[[Category:User manual|The Proving Perspective]]