Skip to content

Commit

Permalink
Harmonisation des noms des contributions: première passe
Browse files Browse the repository at this point in the history 
git-svn-id: svn://scm.gforge.inria.fr/svnroot/coq-contribs/trunk@749 0cf17b13-060f-0410-b1b1-c666bec9822a
  • Loading branch information
notin committed Apr 4, 2008
0 parents commit 2233a0a
Show file tree
Hide file tree
Showing 27 changed files with 20,471 additions and 0 deletions.
2,416 changes: 2,416 additions & 0 deletions BRA-proc.ps.Z.uu

Large diffs are not rendered by default.

21 changes: 21 additions & 0 deletions Make
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
-R . Subst
terminaison_SL.v
sur_les_relations.v
sigma_lift.v
resoudPC_SL.v
lambda_sigma_lift.v
inversionSL.v
egaliteTS.v
determinePC_SL.v
confluence_LSL.v
conf_strong_betapar.v
conf_local_SL.v
comparith.v
commutation.v
betapar.v
Yokouchi.v
TS.v
SLstar_bpar_SLstar.v
Pol2.v
Pol1.v
Newman.v
183 changes: 183 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,183 @@
##########################################################################
## v # The Coq Proof Assistant ##
## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.2 ##
##########################################################################

# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING

#
# This Makefile was generated by the command line :
# coq_makefile -f Make -o Makefile
#

#########################
# #
# Libraries definition. #
# #
#########################

OCAMLLIBS:=
COQLIBS:= -R . Subst
COQDOCLIBS:=-R . Subst

##########################
# #
# Variables definitions. #
# #
##########################

CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)
CAMLP4:=$(notdir $(CAMLP4LIB))
COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
-I $(COQTOP)/library -I $(COQTOP)/parsing \
-I $(COQTOP)/pretyping -I $(COQTOP)/interp \
-I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
-I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \
-I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \
-I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \
-I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \
-I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \
-I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \
-I $(CAMLP4LIB)
ZFLAGS:=$(OCAMLLIBS) $(COQSRC)
OPT:=
COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQC:=$(COQBIN)coqc
COQDEP:=$(COQBIN)coqdep -c
GALLINA:=$(COQBIN)gallina
COQDOC:=$(COQBIN)coqdoc
CAMLC:=$(CAMLBIN)ocamlc -rectypes -c
CAMLOPTC:=$(CAMLBIN)ocamlopt -c
CAMLLINK:=$(CAMLBIN)ocamlc
CAMLOPTLINK:=$(CAMLBIN)ocamlopt
GRAMMARS:=grammar.cma
CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
PP:=-pp "$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl"

###################################
# #
# Definition of the "all" target. #
# #
###################################

VFILES:=terminaison_SL.v\
sur_les_relations.v\
sigma_lift.v\
resoudPC_SL.v\
lambda_sigma_lift.v\
inversionSL.v\
egaliteTS.v\
determinePC_SL.v\
confluence_LSL.v\
conf_strong_betapar.v\
conf_local_SL.v\
comparith.v\
commutation.v\
betapar.v\
Yokouchi.v\
TS.v\
SLstar_bpar_SLstar.v\
Pol2.v\
Pol1.v\
Newman.v
VOFILES:=$(VFILES:.v=.vo)
GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)

all: $(VOFILES)
spec: $(VIFILES)

gallina: $(GFILES)

html: $(GLOBFILES) $(VFILES)
- mkdir html
$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)

gallinahtml: $(GLOBFILES) $(VFILES)
- mkdir html
$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)

all.ps: $(VFILES)
$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`

all-gal.ps: $(VFILES)
$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`



####################
# #
# Special targets. #
# #
####################

.PHONY: all opt byte archclean clean install depend html

%.vo %.glob: %.v
$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*

%.vi: %.v
$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*

%.g: %.v
$(GALLINA) $<

%.tex: %.v
$(COQDOC) -latex $< -o $@

%.html: %.v %.glob
$(COQDOC) -glob-from $*.glob -html $< -o $@

%.g.tex: %.v
$(COQDOC) -latex -g $< -o $@

%.g.html: %.v %.glob
$(COQDOC) -glob-from $*.glob -html -g $< -o $@

%.v.d: %.v
$(COQDEP) -glob -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )

byte:
$(MAKE) all "OPT:=-byte"

opt:
$(MAKE) all "OPT:=-opt"

install:
mkdir -p `$(COQC) -where`/user-contrib
cp -f $(VOFILES) `$(COQC) -where`/user-contrib

Makefile: Make
mv -f Makefile Makefile.bak
$(COQBIN)coq_makefile -f Make -o Makefile


clean:
rm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~
rm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
- rm -rf html

archclean:
rm -f *.cmx *.o


-include $(VFILES:.v=.v.d)
.SECONDARY: $(VFILES:.v=.v.d)

# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING

66 changes: 66 additions & 0 deletions Newman.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,66 @@
(* Contribution to the Coq Library V6.3 (July 1999) *)

(****************************************************************************)
(* The Calculus of Inductive Constructions *)
(* *)
(* Projet Coq *)
(* *)
(* INRIA ENS-CNRS *)
(* Rocquencourt Lyon *)
(* *)
(* Coq V5.10 *)
(* Nov 25th 1994 *)
(* *)
(****************************************************************************)
(* Newman.v *)
(****************************************************************************)

(*****************************************************************************)
(* Projet Coq - Calculus of Inductive Constructions V5.8 *)
(*****************************************************************************)
(* *)
(* Meta-theory of the explicit substitution calculus lambda-env *)
(* Amokrane Saibi *)
(* *)
(* September 1993 *)
(* *)
(*****************************************************************************)


(* Theoreme de Newman *)

Require Import sur_les_relations.

Section NewmanS.
Variable A : Set.
Variable R : A -> A -> Prop.
Hypothesis N : explicit_noetherian _ R.
Hypothesis C : explicit_local_confluence _ R.

Theorem Newman : explicit_confluence _ R.
unfold explicit_confluence in |- *; intro x; pattern x in |- *;
apply (noetherian_induction1 A R N).
intros y H1; unfold confluence_en in |- *.
intros y0 z H2 H3; elim (star_case A R y z H3); intro H4.
exists y0; split.
apply star_refl.
rewrite <- H4; assumption.
elim (star_case A R y y0 H2); intro H5.
exists z; split.
rewrite <- H5; assumption.
apply star_refl.
elim H5; intros y0' H6; elim H6; intros H7 H8.
elim H4; intros z' H9; elim H9; intros H10 H11.
elim (C y y0' z' H7 H10); intros y' H12.
elim H12; intros H13 H14.
elim (H1 y0' H7 y0 y' H8 H13); intros y'' H15.
elim H15; intros H16 H17.
elim (H1 z' H10 y'' z (star_trans A R z' y' y'' H14 H17) H11).
intros u H18; elim H18; intros H19 H20.
exists u; split.
apply star_trans with y''; assumption.
assumption.
Qed.
End NewmanS.


Loading

0 comments on commit 2233a0a

Please sign in to comment.