my_Coq_experiment

learn and try some ideas with Coq.

Name		Name	Last commit message	Last commit date
Latest commit History 10 Commits
#nat_eq_True.v#		#nat_eq_True.v#
Empty_Set_ind_not_like_false_ind.v		Empty_Set_ind_not_like_false_ind.v
Impredicativity_Prop的非直谓性.v		Impredicativity_Prop的非直谓性.v
LICENSE		LICENSE
README.md		README.md
admit_is_false.v		admit_is_false.v
coercion_False_to_Set_to_prove_nat_neq_False.v		coercion_False_to_Set_to_prove_nat_neq_False.v
converse_negative_proposition_not_result_in_origin.v		converse_negative_proposition_not_result_in_origin.v
coq_Art_109.v		coq_Art_109.v
elim (3, 4).v		elim (3, 4).v
eq_comm.v		eq_comm.v
extensionality.v		extensionality.v
forallCommutative.v		forallCommutative.v
inversion策略的复杂性.v		inversion策略的复杂性.v
makeAInversion.v		makeAInversion.v
makeAdiscriminate.v		makeAdiscriminate.v
nat_eq_True.v		nat_eq_True.v
nat_neq_bool.glob		nat_neq_bool.glob
nat_neq_bool.v		nat_neq_bool.v
nat_neq_bool.vo		nat_neq_bool.vo
not_not (not_not_P -> P).v		not_not (not_not_P -> P).v
or_not_and,and_not_or,forall_not_exist,exist_not_forall.v		or_not_and,and_not_or,forall_not_exist,exist_not_forall.v
proove_Prop_Set_Type.v		proove_Prop_Set_Type.v
propositional_extentionality.v		propositional_extentionality.v
reFalse_is_False.v		reFalse_is_False.v
recursive_proof_is_not_allowed.v		recursive_proof_is_not_allowed.v
rewrite_iff.v		rewrite_iff.v
safe head.v		safe head.v
what_does_inversion_do_with_false~=true.v		what_does_inversion_do_with_false~=true.v

Provide feedback