~ubuntu-branches/ubuntu/hardy/coq-doc/hardy

<code class="keyword">Lemma</code> <a name="Extension"></a>Extension : forall B C:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U, B = C -> <a href="Coq.Sets.Ensembles.html#Same_set">Same_set</a> U B C.

<code class="keyword">Proof</code>.

intros B C H'; rewrite H'; auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Lemma</code> <a name="Noone_in_empty"></a>Noone_in_empty : forall x:U, ~ <a href="Coq.Sets.Ensembles.html#In">In</a> U (<a href="Coq.Sets.Ensembles.html#Empty_set">Empty_set</a> U) x.

<code class="keyword">Proof</code>.

red in |- *; destruct 1.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Noone_in_empty">Noone_in_empty</a>.

<code class="keyword">Lemma</code> <a name="Included_Empty"></a>Included_Empty : forall A:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U, <a href="Coq.Sets.Ensembles.html#Included">Included</a> U (<a href="Coq.Sets.Ensembles.html#Empty_set">Empty_set</a> U) A.

<code class="keyword">Proof</code>.

intro; red in |- *.

intros x H; elim (<a href="Coq.Sets.Constructive_sets.html#Noone_in_empty">Noone_in_empty</a> x); auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Included_Empty">Included_Empty</a>.

<code class="keyword">Lemma</code> <a name="Add_intro1"></a>Add_intro1 :

forall (A:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x y:U), <a href="Coq.Sets.Ensembles.html#In">In</a> U A y -> <a href="Coq.Sets.Ensembles.html#In">In</a> U (<code class="keyword">Add</code> U A x) y.

<code class="keyword">Proof</code>.

unfold <code class="keyword">Add</code> at 1 in |- *; auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Add_intro1">Add_intro1</a>.

<code class="keyword">Lemma</code> <a name="Add_intro2"></a>Add_intro2 : forall (A:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x:U), <a href="Coq.Sets.Ensembles.html#In">In</a> U (<code class="keyword">Add</code> U A x) x.

<code class="keyword">Proof</code>.

unfold <code class="keyword">Add</code> at 1 in |- *; auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Add_intro2">Add_intro2</a>.

<code class="keyword">Lemma</code> <a name="Inhabited_add"></a>Inhabited_add : forall (A:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x:U), <a href="Coq.Sets.Ensembles.html#Inhabited">Inhabited</a> U (<code class="keyword">Add</code> U A x).

<code class="keyword">Proof</code>.

intros A x.

apply <a href="Coq.Sets.Ensembles.html#Inhabited_intro">Inhabited_intro</a> with (x:= x); auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Inhabited_add">Inhabited_add</a>.

<code class="keyword">Lemma</code> <a name="Inhabited_not_empty"></a>Inhabited_not_empty :

forall X:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U, <a href="Coq.Sets.Ensembles.html#Inhabited">Inhabited</a> U X -> X <> <a href="Coq.Sets.Ensembles.html#Empty_set">Empty_set</a> U.

<code class="keyword">Proof</code>.

intros X H'; elim H'.

intros x H'0; red in |- *; intro H'1.

absurd (<a href="Coq.Sets.Ensembles.html#In">In</a> U X x); auto with sets.

rewrite H'1; auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Inhabited_not_empty">Inhabited_not_empty</a>.

<code class="keyword">Lemma</code> <a name="Add_not_Empty"></a>Add_not_Empty : forall (A:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x:U), <code class="keyword">Add</code> U A x <> <a href="Coq.Sets.Ensembles.html#Empty_set">Empty_set</a> U.

<code class="keyword">Proof</code>.

auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Add_not_Empty">Add_not_Empty</a>.

<code class="keyword">Lemma</code> <a name="not_Empty_Add"></a>not_Empty_Add : forall (A:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x:U), <a href="Coq.Sets.Ensembles.html#Empty_set">Empty_set</a> U <> <code class="keyword">Add</code> U A x.

<code class="keyword">Proof</code>.

intros; red in |- *; intro H; generalize (<a href="Coq.Sets.Constructive_sets.html#Add_not_Empty">Add_not_Empty</a> A x); auto with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#not_Empty_Add">not_Empty_Add</a>.

<code class="keyword">Lemma</code> <a name="Singleton_inv"></a>Singleton_inv : forall x y:U, <a href="Coq.Sets.Ensembles.html#In">In</a> U (<a href="Coq.Sets.Ensembles.html#Singleton">Singleton</a> U x) y -> x = y.

<code class="keyword">Proof</code>.

intros x y H'; elim H'; trivial with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Singleton_inv">Singleton_inv</a>.

<code class="keyword">Lemma</code> <a name="Singleton_intro"></a>Singleton_intro : forall x y:U, x = y -> <a href="Coq.Sets.Ensembles.html#In">In</a> U (<a href="Coq.Sets.Ensembles.html#Singleton">Singleton</a> U x) y.

<code class="keyword">Proof</code>.

intros x y H'; rewrite H'; trivial with sets.

<code class="keyword">Qed</code>.

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Singleton_intro">Singleton_intro</a>.

100

101

<code class="keyword">Lemma</code> <a name="Union_inv"></a>Union_inv :

102

forall (B C:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x:U), <a href="Coq.Sets.Ensembles.html#In">In</a> U (<a href="Coq.Sets.Ensembles.html#Union">Union</a> U B C) x -> <a href="Coq.Sets.Ensembles.html#In">In</a> U B x \/ <a href="Coq.Sets.Ensembles.html#In">In</a> U C x.

103

<code class="keyword">Proof</code>.

104

intros B C x H'; elim H'; auto with sets.

105

<code class="keyword">Qed</code>.

106

107

108

<code class="keyword">Lemma</code> <a name="Add_inv"></a>Add_inv :

109

forall (A:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x y:U), <a href="Coq.Sets.Ensembles.html#In">In</a> U (<code class="keyword">Add</code> U A x) y -> <a href="Coq.Sets.Ensembles.html#In">In</a> U A y \/ x = y.

110

<code class="keyword">Proof</code>.

111

intros A x y H'; elim H'; auto with sets.

112

<code class="keyword">Qed</code>.

113

114

115

<code class="keyword">Lemma</code> <a name="Intersection_inv"></a>Intersection_inv :

116

forall (B C:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x:U),

117

<a href="Coq.Sets.Ensembles.html#In">In</a> U (<a href="Coq.Sets.Ensembles.html#Intersection">Intersection</a> U B C) x -> <a href="Coq.Sets.Ensembles.html#In">In</a> U B x /\ <a href="Coq.Sets.Ensembles.html#In">In</a> U C x.

118

<code class="keyword">Proof</code>.

119

intros B C x H'; elim H'; auto with sets.

120

<code class="keyword">Qed</code>.

121

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Intersection_inv">Intersection_inv</a>.

122

123

124

<code class="keyword">Lemma</code> <a name="Couple_inv"></a>Couple_inv : forall x y z:U, <a href="Coq.Sets.Ensembles.html#In">In</a> U (<a href="Coq.Sets.Ensembles.html#Couple">Couple</a> U x y) z -> z = x \/ z = y.

125

<code class="keyword">Proof</code>.

126

intros x y z H'; elim H'; auto with sets.

127

<code class="keyword">Qed</code>.

128

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Couple_inv">Couple_inv</a>.

129

130

131

<code class="keyword">Lemma</code> <a name="Setminus_intro"></a>Setminus_intro :

132

forall (A B:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U) (x:U),

133

<a href="Coq.Sets.Ensembles.html#In">In</a> U A x -> ~ <a href="Coq.Sets.Ensembles.html#In">In</a> U B x -> <a href="Coq.Sets.Ensembles.html#In">In</a> U (<a href="Coq.Sets.Ensembles.html#Setminus">Setminus</a> U A B) x.

134

<code class="keyword">Proof</code>.

135

unfold Setminus at 1 in |- *; red in |- *; auto with sets.

136

<code class="keyword">Qed</code>.

137

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Setminus_intro">Setminus_intro</a>.

138

139

<code class="keyword">Lemma</code> <a name="Strict_Included_intro"></a>Strict_Included_intro :

140

forall X Y:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U, <a href="Coq.Sets.Ensembles.html#Included">Included</a> U X Y /\ X <> Y -> <a href="Coq.Sets.Ensembles.html#Strict_Included">Strict_Included</a> U X Y.

141

<code class="keyword">Proof</code>.

142

auto with sets.

143

<code class="keyword">Qed</code>.

144

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Strict_Included_intro">Strict_Included_intro</a>.

145

146

147

<code class="keyword">Lemma</code> <a name="Strict_Included_strict"></a>Strict_Included_strict : forall X:<a href="Coq.Sets.Ensembles.html#Ensemble">Ensemble</a> U, ~ <a href="Coq.Sets.Ensembles.html#Strict_Included">Strict_Included</a> U X X.

148

<code class="keyword">Proof</code>.

149

intro X; red in |- *; intro H'; elim H'.

150

intros H'0 H'1; elim H'1; auto with sets.

151

<code class="keyword">Qed</code>.

152

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Strict_Included_strict">Strict_Included_strict</a>.

153

154

155

<code class="keyword">End</code> Ensembles_facts.

156

157

158

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Constructive_sets.html#Singleton_inv">Singleton_inv</a> <a href="Coq.Sets.Constructive_sets.html#Singleton_intro">Singleton_intro</a> <a href="Coq.Sets.Constructive_sets.html#Add_intro1">Add_intro1</a> <a href="Coq.Sets.Constructive_sets.html#Add_intro2">Add_intro2</a>

159

<a href="Coq.Sets.Constructive_sets.html#Intersection_inv">Intersection_inv</a> <a href="Coq.Sets.Constructive_sets.html#Couple_inv">Couple_inv</a> <a href="Coq.Sets.Constructive_sets.html#Setminus_intro">Setminus_intro</a> <a href="Coq.Sets.Constructive_sets.html#Strict_Included_intro">Strict_Included_intro</a>

160

<a href="Coq.Sets.Constructive_sets.html#Strict_Included_strict">Strict_Included_strict</a> <a href="Coq.Sets.Constructive_sets.html#Noone_in_empty">Noone_in_empty</a> <a href="Coq.Sets.Constructive_sets.html#Inhabited_not_empty">Inhabited_not_empty</a> <a href="Coq.Sets.Constructive_sets.html#Add_not_Empty">Add_not_Empty</a>

161

<a href="Coq.Sets.Constructive_sets.html#not_Empty_Add">not_Empty_Add</a> <a href="Coq.Sets.Constructive_sets.html#Inhabited_add">Inhabited_add</a> <a href="Coq.Sets.Constructive_sets.html#Included_Empty">Included_Empty</a>: sets v62.</code>

162

<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a>

163

</body>

164

</html>

b'\\ No newline at end of file'

Older »