Datatype Rules - Revision history

imported>Nicolas: /* Datatypes used */

2010-09-07T13:37:11Z

Datatypes used

← Older revision		Revision as of 13:37, 7 September 2010
Line 37:		Line 37:

	Let us have a function		Let us have a function
	<math>\operatorname{height} \in \operatorname{Tree} \tfun \N</math> defining the height of a tree		<math>\operatorname{height} \in \operatorname{Tree} \tfun \N</math>
			defining the height of a tree

	== Distinct Case ==		== Distinct Case ==

imported>Nicolas: removed application of auto eh in right part of sequents

2010-09-07T13:25:30Z

removed application of auto eh in right part of sequents

← Older revision		Revision as of 13:25, 7 September 2010
Line 46:		Line 46:


	=== ~~Application to~~ directions ===		=== Distinct Case on directions ===


Line 55:		Line 55:

	The resulting proof step is		The resulting proof step is
	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{north}~~) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{east}~~) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{south}~~) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{west}~~) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>		<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

	further simplifications depend on the existence of rules about move and the various directions.		further simplifications depend on the existence of rules about move and the various directions.

	=== ~~Application to~~ lists ===		=== Distinct Case on lists ===

	Starting from goal		Starting from goal
Line 67:		Line 67:
	we can free variable l then apply Distinct Case on it:		we can free variable l then apply Distinct Case on it:

	<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,~~\operatorname{nil}~~) \land (\forall y \qdot \operatorname{member}(y,~~\operatorname{nil}~~) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,~~\operatorname{cons}(head0, tail1)~~) \land (\forall y \qdot \operatorname{member}(y,~~\operatorname{cons}(head0, tail1)~~) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>		<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>

	The left antecedent shows that the case of the nil list has been forgotten when writing the theorem.		The left antecedent shows that the case of the nil list has been forgotten when writing the theorem. The right antecedent looks as hard to prove as the initial goal (but see [[#Induction on lists\|the induction application]]).

	=== ~~Application to~~ trees ===		=== Distinct Case on trees ===

	Starting from goal		Starting from goal
Line 79:		Line 79:
	we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:		we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:

	<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(~~\operatorname{empty}~~) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(~~\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})~~) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>		<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(t) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(t) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>

	the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.		the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.
Line 91:		Line 91:
	The only difference with Distinct Case resides in the <math>\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})</math> hypotheses for inductive parameters.		The only difference with Distinct Case resides in the <math>\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})</math> hypotheses for inductive parameters.

	=== ~~Application to~~ directions ===		=== Induction on directions ===


Line 100:		Line 100:

	The resulting proof step is		The resulting proof step is
	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{north}~~) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{east}~~) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{south}~~) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{west}~~) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>		<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

	As we can see, it is exactly the same proof step as for Distinct Case: the reason is that the direction constructors contain no parameters, a fortiori no inductive parameters, so there are no additional hypotheses.		As we can see, it is exactly the same proof step as for Distinct Case: the reason is that the direction constructors contain no parameters, a fortiori no inductive parameters, so there are no additional hypotheses.

	=== ~~Application to~~ lists ===		=== Induction on lists ===

	Starting from goal		Starting from goal
Line 112:		Line 112:
	we can free variable l then apply Induction on it:		we can free variable l then apply Induction on it:

	<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,~~\operatorname{nil}~~) \land (\forall y \qdot \operatorname{member}(y,~~\operatorname{nil}~~) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;,\; \exists x \qdot \operatorname{member}(x,tail1) \land (\forall y \qdot \operatorname{member}(y,tail1) \limp y \leq x) \;\vdash \; \exists x \qdot \operatorname{member}(x,~~\operatorname{cons}(head0, tail1)~~) \land (\forall y \qdot \operatorname{member}(y,~~\operatorname{cons}(head0, tail1)~~) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>		<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;,\; \exists x \qdot \operatorname{member}(x,tail1) \land (\forall y \qdot \operatorname{member}(y,tail1) \limp y \leq x) \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>

	The left antecedent shows the same problem as Distinct for nil list. The benefit of the Induction is in the right antecedent with the additional hypothesis that the predicate stands for tail1. Next step will be to free the x in the tail1 hypothesis, then use it to instantiate the x in the goal with <math>\operatorname{max}(\operatorname{head0}, x_{\operatorname{tail1}})</math>.		The left antecedent shows the same problem as Distinct for nil list. The benefit of the Induction is in the right antecedent with the additional hypothesis that the predicate stands for tail1. Next step will be to make eh on l, free the x in the tail1 hypothesis, then use it to instantiate the x in the goal with <math>\operatorname{max}(\operatorname{head0}, x_{\operatorname{tail1}})</math>.
	In this proof, application of Distinct Case does not allow to complete the proof (at least not so easily), whereas Induction does.		In this proof, application of Distinct Case does not allow to complete the proof (at least not so easily), whereas Induction does.

	=== ~~Application to~~ trees ===		=== Induction on trees ===

	Starting from goal		Starting from goal
Line 127:		Line 127:
	<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;,\;\; \operatorname{height}(\operatorname{left0}) < \operatorname{height}(t) \;,\;\; \operatorname{height}(\operatorname{right2}) < \operatorname{height}(t) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>		<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;,\;\; \operatorname{height}(\operatorname{left0}) < \operatorname{height}(t) \;,\;\; \operatorname{height}(\operatorname{right2}) < \operatorname{height}(t) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>

	the left antecedent will then be proved using the contradiction in hypotheses. In the right one, additional induction hypotheses do not provide much help: ~~we are~~ in a situation ~~very similar to the one after applying~~ Distinct Case~~. It can be more appropriate~~ to ~~free only~~ the ~~t variable, then apply induction to the whole predicate: <math>\forall l,v,r \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>~~		the left antecedent will then be proved using the contradiction in hypotheses. In the right one, additional induction hypotheses do not provide much help: in this situation, using Distinct Case and properties about height is sufficient to discharge the proof.

	~~that gives the following right antecedent:~~
	~~<math>t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})</math>~~
	~~<math>\forall l,v,r \qdot \operatorname{left0} = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(\operatorname{left0})</math>~~
	~~<math>\forall l,v,r \qdot \operatorname{right2} = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(\operatorname{right2})</math>~~
	~~<math>\vdash</math>~~
	~~<math>\forall l,v,r \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>~~

imported>Nicolas: Induction

2010-09-07T11:48:16Z

Induction

← Older revision		Revision as of 11:48, 7 September 2010
Line 85:		Line 85:
	== Induction ==		== Induction ==

	{{~~TODO~~}}		The rule states

			<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>

			The only difference with Distinct Case resides in the <math>\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})</math> hypotheses for inductive parameters.

			=== Application to directions ===


			Starting from goal
			<math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math>

			we can free variables x,y,d then apply Induction on d:

			The resulting proof step is
			<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

			As we can see, it is exactly the same proof step as for Distinct Case: the reason is that the direction constructors contain no parameters, a fortiori no inductive parameters, so there are no additional hypotheses.

			=== Application to lists ===

			Starting from goal

			<math>\forall l \qdot \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)</math>

			we can free variable l then apply Induction on it:

			<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{nil}) \land (\forall y \qdot \operatorname{member}(y,\operatorname{nil}) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;,\; \exists x \qdot \operatorname{member}(x,tail1) \land (\forall y \qdot \operatorname{member}(y,tail1) \limp y \leq x) \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{cons}(head0, tail1)) \land (\forall y \qdot \operatorname{member}(y,\operatorname{cons}(head0, tail1)) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>

			The left antecedent shows the same problem as Distinct for nil list. The benefit of the Induction is in the right antecedent with the additional hypothesis that the predicate stands for tail1. Next step will be to free the x in the tail1 hypothesis, then use it to instantiate the x in the goal with <math>\operatorname{max}(\operatorname{head0}, x_{\operatorname{tail1}})</math>.
			In this proof, application of Distinct Case does not allow to complete the proof (at least not so easily), whereas Induction does.

			=== Application to trees ===

			Starting from goal

			<math>\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>

			we can free variables l,v,r,t then apply IMP_R and then Induction on t:

			<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;,\;\; \operatorname{height}(\operatorname{left0}) < \operatorname{height}(t) \;,\;\; \operatorname{height}(\operatorname{right2}) < \operatorname{height}(t) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>

			the left antecedent will then be proved using the contradiction in hypotheses. In the right one, additional induction hypotheses do not provide much help: we are in a situation very similar to the one after applying Distinct Case. It can be more appropriate to free only the t variable, then apply induction to the whole predicate: <math>\forall l,v,r \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>

			that gives the following right antecedent:
			<math>t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})</math>
			<math>\forall l,v,r \qdot \operatorname{left0} = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(\operatorname{left0})</math>
			<math>\forall l,v,r \qdot \operatorname{right2} = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(\operatorname{right2})</math>
			<math>\vdash</math>
			<math>\forall l,v,r \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>

imported>Nicolas: /* Application to trees */

2010-09-06T17:43:35Z

Application to trees

← Older revision		Revision as of 17:43, 6 September 2010
Line 75:		Line 75:
	Starting from goal		Starting from goal

	<math>\forall l,v,r,t. t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>		<math>\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>

	we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:		we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:

	<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>		<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>

			the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.

	== Induction ==		== Induction ==

	{{TODO}}		{{TODO}}

imported>Nicolas at 17:15, 6 September 2010

2010-09-06T17:15:58Z

← Older revision		Revision as of 17:15, 6 September 2010
Line 52:		Line 52:
	<math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math>		<math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math>

	we can free variables x,y,d then apply Distinct Case:		we can free variables x,y,d then apply Distinct Case on d:

	The resulting proof step is		The resulting proof step is
Line 73:		Line 73:
	=== Application to trees ===		=== Application to trees ===

	{{~~TODO~~}}		Starting from goal

			<math>\forall l,v,r,t. t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>

			we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:

	!l,v,r. t = node(l,v,r) => height(l) < height(t)		<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>

	== Induction ==		== Induction ==

	{{TODO}}		{{TODO}}

imported>Nicolas: /* Application to lists */

2010-09-06T17:02:04Z

Application to lists

← Older revision		Revision as of 17:02, 6 September 2010
Line 67:		Line 67:
	we can free variable l then apply Distinct Case on it:		we can free variable l then apply Distinct Case on it:

			<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{nil}) \land (\forall y \qdot \operatorname{member}(y,\operatorname{nil}) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{cons}(head0, tail1)) \land (\forall y \qdot \operatorname{member}(y,\operatorname{cons}(head0, tail1)) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>

	~~This~~ shows that nil list has been forgotten in the ~~predicate~~.		The left antecedent shows that the case of the nil list has been forgotten when writing the theorem.

	=== Application to trees ===		=== Application to trees ===

imported>Nicolas: /* Application to lists */

2010-09-06T16:53:24Z

Application to lists

← Older revision		Revision as of 16:53, 6 September 2010
Line 61:		Line 61:
	=== Application to lists ===		=== Application to lists ===

	~~{{TODO}}~~		Starting from goal

	!l ~~oftype list(~~\~~Z). #~~x. member(x,l) & (!y. member(y,l) => y <= x)		<math>\forall l \qdot \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)</math>

	~~evidence~~ that nil list has been forgotten in the predicate		we can free variable l then apply Distinct Case on it:


			This shows that nil list has been forgotten in the predicate.

	=== Application to trees ===		=== Application to trees ===

imported>Nicolas: /* Application to directions */

2010-09-06T16:49:05Z

Application to directions

← Older revision		Revision as of 16:49, 6 September 2010
Line 55:		Line 55:

	The resulting proof step is		The resulting proof step is
	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=east \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=south \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=west \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>		<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

	further simplifications depend on the existence of rules about move and the various directions.		further simplifications depend on the existence of rules about move and the various directions.

imported>Nicolas: /* Application to directions */

2010-09-06T16:47:54Z

Application to directions

← Older revision		Revision as of 16:47, 6 September 2010
Line 54:		Line 54:
	we can free variables x,y,d then apply Distinct Case:		we can free variables x,y,d then apply Distinct Case:

	\|		The resulting proof step is
	~~\| south~~
	~~\| west~~
	The resulting ~~sequent~~ is
	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=east \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=south \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=west \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>		<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=east \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=south \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=west \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

imported>Nicolas: applying DC to directions

2010-09-06T16:46:42Z

applying DC to directions

← Older revision		Revision as of 16:46, 6 September 2010
Line 48:		Line 48:
	=== Application to directions ===		=== Application to directions ===

	~~{{TODO}}~~

	!x,y,~~dir .~~ move(x,y,~~dir~~) /= x \|-> y		Starting from goal
			<math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math>

			we can free variables x,y,d then apply Distinct Case:

			\|
			\| south
			\| west
			The resulting sequent is
			<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=east \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=south \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=west \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

			further simplifications depend on the existence of rules about move and the various directions.

	=== Application to lists ===		=== Application to lists ===
Line 64:		Line 74:
	{{TODO}}		{{TODO}}

			!l,v,r. t = node(l,v,r) => height(l) < height(t)

	== Induction ==		== Induction ==

	{{TODO}}		{{TODO}}