Maplet Overriding in Goal - Revision history

imported>Laurent at 16:05, 18 March 2014

2014-03-18T16:05:41Z

← Older revision		Revision as of 16:05, 18 March 2014
Line 178:		Line 178:


	[[Category:Design ~~proposal~~]]		[[Category:Design]]

imported>Billaude: Mapplet Overriding in Goal moved to Maplet Overriding in Goal: Spelling mistake.

2011-09-26T12:22:30Z

Mapplet Overriding in Goal moved to Maplet Overriding in Goal: Spelling mistake.

← Older revision	Revision as of 12:22, 26 September 2011
(No difference)

imported>Billaude: /* Table */

2011-09-19T13:21:52Z

Table

← Older revision		Revision as of 13:21, 19 September 2011
Line 67:		Line 67:
	\|<math>-</math>		\|<math>-</math>
	\|<math>-</math>		\|<math>-</math>
	\|<math>-</math>		\|<math>\checkmark</math>
	\|<math>\checkmark</math>		\|<math>\checkmark</math>
	\|<math>\checkmark</math>		\|<math>\checkmark</math>

imported>Billaude at 06:21, 6 September 2011

2011-09-06T06:21:53Z

← Older revision		Revision as of 06:21, 6 September 2011
Line 52:		Line 52:
	\|<math>-</math>		\|<math>-</math>
	\|<math>\checkmark</math>		\|<math>\checkmark</math>
	\|<math></math>		\|<math>-</math>
	\|<math>\checkmark</math>		\|<math>\checkmark</math>
	\|<math>-</math>		\|<math>-</math>

imported>Billaude: Rules implemented in MapOvrGoal have been changed. Modifications have been reported their.

2011-09-05T14:41:57Z

Rules implemented in MapOvrGoal have been changed. Modifications have been reported their.

Show changes

imported>Billaude: /* Implementation */

2011-08-19T16:03:36Z

Implementation

← Older revision		Revision as of 16:03, 19 August 2011
Line 15:		Line 15:
	But, we know that <math>\left(f\in A\;op\;B\right)\limp \left(\{x\}\domsub f\in A\setminus\{x\}\;op\;B\right)</math>. By ensuring that this predicate is among the hypotheses of the sequent, we are sure that it will be proofed. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writing <math>f\in A\;op\;B</math> instead of <math>\{x\}\domsub f\in A\setminus\{x\}\;op\;B</math>.		But, we know that <math>\left(f\in A\;op\;B\right)\limp \left(\{x\}\domsub f\in A\setminus\{x\}\;op\;B\right)</math>. By ensuring that this predicate is among the hypotheses of the sequent, we are sure that it will be proofed. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writing <math>f\in A\;op\;B</math> instead of <math>\{x\}\domsub f\in A\setminus\{x\}\;op\;B</math>.

	~~= Implementation =~~

	~~First, the goal is checked. Its tree structure must match the following one :~~
	~~<math>\in</math>~~
	~~├── <math>\ovl</math>~~
	~~│ ├── f~~
	~~│ └── {}~~
	~~│ └── <math>\mapsto</math>~~
	~~│ ├── x~~
	~~│ └── y~~
	~~└── <math>op</math>~~
	~~├── A~~
	~~└── B~~
	~~Then, if the hypothesis <math>f\in A\to B</math> is present, the goal is split as follows :~~
	~~:*<math>f\in A\;op\;B</math>~~
	~~:*<math>x \in A</math>~~
	~~:*<math>y \in B</math>~~
	~~Else nothing is proceeded.~~

	[[Category:Design proposal]]		[[Category:Design proposal]]

imported>Billaude at 14:41, 19 August 2011

2011-08-19T14:41:28Z

← Older revision		Revision as of 14:41, 19 August 2011
Line 3:		Line 3:
	= Objective =		= Objective =

	Split every goal in the form : <math> f \ovl{\{x \mapsto y\}} \in A \to B </math> into three sub-goals :		Split every goal in the form : <math>f\ovl{\{x\mapsto y\}}\in A\to B </math> into three sub-goals if and only if the sequent contains that hypothesis <math>f\in A\;op\;B</math> :
	:*<math>~~\{x\} \domsub~~ f \in A \~~smallsetminus~~ \~~{x\} \to~~ B</math>		:*<math>f\in A\;op\;B</math>
	:*<math>x \in A</math>		:*<math>x\in A</math>
	:*<math>y \in B</math>		:*<math>y\in B</math>
			Where <math>op</math> denote either a Relation <math>\left(\rel\right)</math>, or a Total Relation <math>\left(\trel\right)</math>, or a Partial Function <math>\left(\pfun\right)</math>, or a Total Function <math>\left(\tfun\right)</math>.

	= Design Decision =		= Design Decision =

	~~Instead of proofing~~ the ~~first sub-~~goal, ~~it may be more easy to proof~~ <math>f\in A\to B</math> ~~which~~ is ~~a sufficient condition :~~ <math>(f\in A\to B)\limp (\{x\} \domsub f \in A \~~smallsetminus~~ \{x\} \to B)</math>.		Those three subgoals are not equivalent to the goal from which they are inferred. In order to get the equivalence, we should write <math>\{x\}\domsub f\in A\setminus\{x\}\;op\;B</math>. But this has the drawback of writing twice the expression ''x''. If this expression is big, then it can make the proof rule hard to read.

			But, we know that <math>\left(f\in A\;op\;B\right)\limp \left(\{x\}\domsub f\in A\setminus\{x\}\;op\;B\right)</math>. By ensuring that this predicate is among the hypotheses of the sequent, we are sure that it will be proofed. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writing <math>f\in A\;op\;B</math> instead of <math>\{x\}\domsub f\in A\setminus\{x\}\;op\;B</math>.

	= Implementation =		= Implementation =
Line 22:		Line 25:
	│ ├── x		│ ├── x
	│ └── y		│ └── y
	└── <math>~~\to~~</math>		└── <math>op</math>
	├── A		├── A
	└── B		└── B
	Then, if the hypothesis <math>f\in A\to B</math> is present, the goal is split as follows :		Then, if the hypothesis <math>f\in A\to B</math> is present, the goal is split as follows :
	:*<math>f\in A\~~to B</math>~~		:*<math>f\in A\;op\;B</math>
	~~:*<math>x~~ \~~in A</math>~~
	~~:*<math>y \in B</math>~~
	~~Else, it is split as follows :~~
	~~:*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to~~ B</math>
	:*<math>x \in A</math>		:*<math>x \in A</math>
	:*<math>y \in B</math>		:*<math>y \in B</math>
			Else nothing is proceeded.

	[[Category:Design proposal]]		[[Category:Design proposal]]

imported>Billaude: /* Implementation */

2011-05-30T13:11:34Z

Implementation

← Older revision		Revision as of 13:11, 30 May 2011
Line 25:		Line 25:
	├── A		├── A
	└── B		└── B
	Then, if the hypothesis <math>f\in A\to B</math> is ~~contained in the hypothesis~~ the goal is ~~splitted~~ as follows :		Then, if the hypothesis <math>f\in A\to B</math> is present, the goal is split as follows :
	:*<math>f\in A\to B</math>		:*<math>f\in A\to B</math>
	:*<math>x \in A</math>		:*<math>x \in A</math>
	:*<math>y \in B</math>		:*<math>y \in B</math>
	Else, it is ~~splitted~~ as follows :		Else, it is split as follows :
	:*<math>{x} \domsub f \in A \smallsetminus ~~\left~~\{x~~\right~~\} \to B</math>		:*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to B</math>
	:*<math>x \in A</math>		:*<math>x \in A</math>
	:*<math>y \in B</math>		:*<math>y \in B</math>

	[[Category:Design proposal]]		[[Category:Design proposal]]

imported>Billaude: /* Design Decision */

2011-05-30T13:09:04Z

Design Decision

← Older revision		Revision as of 13:09, 30 May 2011
Line 10:		Line 10:
	= Design Decision =		= Design Decision =

	Instead of proofing the first sub-goal, it may be more easy to proof <math>f\in A\to B</math> which is a sufficient condition : <math>(f\in A\to B)\limp ({x} \domsub f \in A \smallsetminus ~~\left~~\{x~~\right~~\} \to B)</math>.		Instead of proofing the first sub-goal, it may be more easy to proof <math>f\in A\to B</math> which is a sufficient condition : <math>(f\in A\to B)\limp (\{x\} \domsub f \in A \smallsetminus \{x\} \to B)</math>.

	= Implementation =		= Implementation =

imported>Billaude: /* Objective */

2011-05-30T13:08:31Z

Objective

← Older revision		Revision as of 13:08, 30 May 2011
Line 3:		Line 3:
	= Objective =		= Objective =

	Split every goal in the form : <math> f \ovl{~~\left~~\{x \mapsto y~~\right~~\}} \in A \to B </math> into three sub-goals :		Split every goal in the form : <math> f \ovl{\{x \mapsto y\}} \in A \to B </math> into three sub-goals :
	:*<math>{x} \domsub f \in A \smallsetminus ~~\left~~\{x~~\right~~\} \to B</math>		:*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to B</math>
	:*<math>x \in A</math>		:*<math>x \in A</math>
	:*<math>y \in B</math>		:*<math>y \in B</math>