Linguist 2.3.0

Closes #206

README.md

@@ -8,7 +8,9 @@ We use this library at GitHub to detect blob languages, highlight code, ignore b
 
 Linguist defines the list of all languages known to GitHub in a [yaml file](https://github.com/github/linguist/blob/master/lib/linguist/languages.yml). In order for a file to be highlighted, a language and lexer must be defined there.
 
-Most languages are detected by their file extension. This is the fastest and most common situation. For script files, which are usually extensionless, we do "deep content inspection"™ and check the shebang of the file. Checking the file's contents may also be used for disambiguating languages. C, C++ and Obj-C all use `.h` files. Looking for common keywords, we are usually able to guess the correct language.
+Most languages are detected by their file extension. This is the fastest and most common situation.
+
+For disambiguating between files with common extensions, we use a [bayesian classifier](https://github.com/github/linguist/blob/master/lib/linguist/classifier.rb). For an example, this helps us tell the difference between `.h` files which could be either C, C++, or Obj-C.
 
 In the actual GitHub app we deal with `Grit::Blob` objects. For testing, there is a simple `FileBlob` API.
 
@@ -22,23 +24,11 @@ See [lib/linguist/language.rb](https://github.com/github/linguist/blob/master/li
 
 The actual syntax highlighting is handled by our Pygments wrapper, [pygments.rb](https://github.com/tmm1/pygments.rb). It also provides a [Lexer abstraction](https://github.com/tmm1/pygments.rb/blob/master/lib/pygments/lexer.rb) that determines which highlighter should be used on a file.
 
-We typically run on a prerelease version of Pygments to get early access to new lexers. The [lexers.yml](https://github.com/github/linguist/blob/master/lib/linguist/lexers.yml) file is a dump of the lexers we have available on our server. If there is a new lexer in pygments-main not on the list, [open an issue](https://github.com/github/linguist/issues) and we'll try to upgrade it soon.
-
-### MIME type detection
-
-Most of the MIME types handling is done by the Ruby [mime-types gem](https://github.com/halostatue/mime-types). But we have our own list of additions and overrides. To add or modify this list, see [lib/linguist/mimes.yml](https://github.com/github/linguist/blob/master/lib/linguist/mimes.yml).
-
-MIME types are used to set the Content-Type of raw binary blobs which are served from a special `raw.github.com` domain. However, all text blobs are served as `text/plain` regardless of their type to ensure they open in the browser rather than downloading.
-
-The MIME type also determines whether a blob is binary or plain text. So if you're seeing a blob that says "View Raw" and it is actually plain text, the mime type and encoding probably needs to be explicitly stated.
-
-    Linguist::FileBlob.new("linguist.zip").binary? #=> true
-
-See [lib/linguist/mimes.yml](https://github.com/github/linguist/blob/master/lib/linguist/mimes.yml).
+We typically run on a prerelease version of Pygments, [pygments.rb](https://github.com/tmm1/pygments.rb), to get early access to new lexers. The [lexers.yml](https://github.com/github/linguist/blob/master/lib/linguist/lexers.yml) file is a dump of the lexers we have available on our server.
 
 ### Stats
 
-The [Language Graph](https://github.com/github/linguist/graphs/languages) is built by aggregating the languages of all repo's blobs. The top language in the graph determines the project's primary language. Collectively, these stats make up the [Top Languages](https://github.com/languages) page.
+The Language Graph you see on every repository is built by aggregating the languages of all repo's blobs. The top language in the graph determines the project's primary language. Collectively, these stats make up the [Top Languages](https://github.com/languages) page.
 
 The repository stats API can be used on a directory:
 
@@ -70,7 +60,9 @@ See [Linguist::BlobHelper#generated?](https://github.com/github/linguist/blob/ma
 
 ## Installation
 
-To get it, clone the repo and run [Bundler](http://gembundler.com/) to install its dependencies.
+github.com is usually running the latest version of the `github-linguist` gem that is released on [RubyGems.org](http://rubygems.org/gems/github-linguist).
+
+But for development you are going to want to checkout out the source. To get it, clone the repo and run [Bundler](http://gembundler.com/) to install its dependencies.
 
     git clone https://github.com/github/linguist.git
     cd linguist/
@@ -80,17 +72,14 @@ To run the tests:
 
     bundle exec rake test
 
-*Since this code is specific to GitHub, is not published as a official rubygem.*
-
-If you are seeing errors like `StandardError: could not find any magic files!`, it means the CharlockHolmes gem didn’t install correctly. See the [installing section](https://github.com/brianmario/charlock_holmes/blob/master/README.md) of the CharlockHolmes README for more information.
-
 ## Contributing
 
-1. Fork it.
-2. Create a branch (`git checkout -b detect-foo-language`)
-3. Make your changes
-4. Run the tests (`bundle install` then `bundle exec rake`)
-5. Commit your changes (`git commit -am "Added detection for the new Foo language"`)
-6. Push to the branch (`git push origin detect-foo-language`)
-7. Create a [Pull Request](http://help.github.com/pull-requests/) from your branch.
-8. Promote it. Get others to drop in and +1 it.
+The majority of patches won't need to touch any Ruby code at all. The [master language list](https://github.com/github/linguist/blob/master/lib/linguist/languages.yml) is just a configuration file.
+
+Almost all bug fixes or new language additions should come with some additional code samples. Just drop them under [`samples/`](https://github.com/github/linguist/tree/master/samples) in the correct subdirectory and our test suite will automatically test them. In most cases you shouldn't need to add any new assertions.
+
+### Testing
+
+Sometimes getting the tests running can be to much work especially if you don't have much Ruby experience. Its okay, be lazy and let our build bot [Travis](http://travis-ci.org/#!/github/linguist) run the tests for you. Just open a pull request and the bot will start cranking away.
+
+Heres our current build status, which is hopefully green: [![Build Status](https://secure.travis-ci.org/github/linguist.png?branch=master)](http://travis-ci.org/github/linguist)

Rakefile

@@ -7,23 +7,21 @@ Rake::TestTask.new do |t|
   t.warning = true
 end
 
-
-file 'lib/linguist/classifier.yml' => Dir['test/fixtures/**/*'] do |f|
-  require 'linguist/sample'
-  classifier = Linguist::Sample.classifier
-  File.open(f.name, 'w') { |io| YAML.dump(classifier, io) }
+task :samples do
+  require 'linguist/samples'
+  require 'yajl'
+  data = Linguist::Samples.data
+  json = Yajl::Encoder.encode(data, :pretty => true)
+  File.open('lib/linguist/samples.json', 'w') { |io| io.write json }
 end
 
-CLOBBER.include 'lib/linguist/classifier.yml'
-
-task :classifier => ['lib/linguist/classifier.yml']
-
 namespace :classifier do
   LIMIT = 1_000
 
   desc "Run classifier against #{LIMIT} public gists"
   task :test do
     require 'linguist/classifier'
+    require 'linguist/samples'
 
     total, correct, incorrect = 0, 0, 0
     $stdout.sync = true
@@ -32,10 +30,10 @@ namespace :classifier do
       next if file_language.nil? || file_language == 'Text'
       begin
         data = open(file_url).read
-        guessed_language, score = Linguist::Classifier.instance.classify(data).first
+        guessed_language, score = Linguist::Classifier.classify(Linguist::Samples::DATA, data).first
 
         total += 1
-        guessed_language.name == file_language ? correct += 1 : incorrect += 1
+        guessed_language == file_language ? correct += 1 : incorrect += 1
 
         print "\r\e[0K%d:%d  %g%%" % [correct, incorrect, (correct.to_f/total.to_f)*100]
         $stdout.flush

bin/linguist

@@ -23,12 +23,11 @@ elsif File.file?(path)
 
   puts "#{blob.name}: #{blob.loc} lines (#{blob.sloc} sloc)"
   puts "  type:      #{type}"
-  puts "  extension: #{blob.pathname.extname}"
   puts "  mime type: #{blob.mime_type}"
   puts "  language:  #{blob.language}"
 
   if blob.large?
-    puts "  blob is to large to be shown"
+    puts "  blob is too large to be shown"
   end
 
   if blob.generated?

github-linguist.gemspec

@@ -1,6 +1,6 @@
 Gem::Specification.new do |s|
   s.name    = 'github-linguist'
-  s.version = '2.0.0'
+  s.version = '2.3.0'
   s.summary = "GitHub Language detection"
 
   s.authors = "GitHub"
@@ -10,8 +10,9 @@ Gem::Specification.new do |s|
 
   s.add_dependency 'charlock_holmes', '~> 0.6.6'
   s.add_dependency 'escape_utils',    '~> 0.2.3'
-  s.add_dependency 'mime-types',      '~> 1.18'
-  s.add_dependency 'pygments.rb',     '~> 0.2.13'
+  s.add_dependency 'mime-types',      '~> 1.19'
+  s.add_dependency 'pygments.rb',     '>= 0.2.13'
   s.add_development_dependency 'json'
   s.add_development_dependency 'rake'
+  s.add_development_dependency 'yajl-ruby'
 end

lib/linguist.rb

@@ -1,5 +1,5 @@
 require 'linguist/blob_helper'
+require 'linguist/generated'
 require 'linguist/language'
-require 'linguist/mime'
-require 'linguist/pathname'
 require 'linguist/repository'
+require 'linguist/samples'

lib/linguist/blob_helper.rb

@@ -1,10 +1,9 @@
-require 'linguist/classifier'
+require 'linguist/generated'
 require 'linguist/language'
-require 'linguist/mime'
-require 'linguist/pathname'
 
 require 'charlock_holmes'
 require 'escape_utils'
+require 'mime/types'
 require 'pygments'
 require 'yaml'
 
@@ -12,13 +11,6 @@ module Linguist
   # BlobHelper is a mixin for Blobish classes that respond to "name",
   # "data" and "size" such as Grit::Blob.
   module BlobHelper
-    # Internal: Get a Pathname wrapper for Blob#name
-    #
-    # Returns a Pathname.
-    def pathname
-      Pathname.new(name || "")
-    end
-
     # Public: Get the extname of the path
     #
     # Examples
@@ -28,7 +20,23 @@ module Linguist
     #
     # Returns a String
     def extname
-      pathname.extname
+      File.extname(name.to_s)
+    end
+
+    # Internal: Lookup mime type for extension.
+    #
+    # Returns a MIME::Type
+    def _mime_type
+      if defined? @_mime_type
+        @_mime_type
+      else
+        guesses = ::MIME::Types.type_for(extname.to_s)
+
+        # Prefer text mime types over binary
+        @_mime_type = guesses.detect { |type| type.ascii? } ||
+          # Otherwise use the first guess
+          guesses.first
+      end
     end
 
     # Public: Get the actual blob mime type
@@ -40,7 +48,14 @@ module Linguist
     #
     # Returns a mime type String.
     def mime_type
-      @mime_type ||= pathname.mime_type
+      _mime_type ? _mime_type.to_s : 'text/plain'
+    end
+
+    # Internal: Is the blob binary according to its mime type
+    #
+    # Return true or false
+    def binary_mime_type?
+      _mime_type ? _mime_type.binary? : false
     end
 
     # Public: Get the Content-Type header value
@@ -72,7 +87,7 @@ module Linguist
       elsif name.nil?
         "attachment"
       else
-        "attachment; filename=#{EscapeUtils.escape_url(pathname.basename)}"
+        "attachment; filename=#{EscapeUtils.escape_url(File.basename(name))}"
       end
     end
 
@@ -91,15 +106,6 @@ module Linguist
       @detect_encoding ||= CharlockHolmes::EncodingDetector.new.detect(data) if data
     end
 
-    # Public: Is the blob binary according to its mime type
-    #
-    # Return true or false
-    def binary_mime_type?
-      if mime_type = Mime.lookup_mime_type_for(pathname.extname)
-        mime_type.binary?
-      end
-    end
-
     # Public: Is the blob binary?
     #
     # Return true or false
@@ -136,22 +142,6 @@ module Linguist
       ['.png', '.jpg', '.jpeg', '.gif'].include?(extname)
     end
 
-    # Public: Is the blob a possible drupal php file?
-    #
-    # Return true or false
-    def drupal_extname?
-      ['.module', '.install', '.test', '.inc'].include?(extname)
-    end
-
-    # Public: Is the blob likely to have a shebang?
-    #
-    # Return true or false
-    def shebang_extname?
-      extname.empty? &&
-        mode &&
-        (mode.to_i(8) & 05) == 05
-    end
-
     MEGABYTE = 1024 * 1024
 
     # Public: Is the blob too big to load?
@@ -235,143 +225,16 @@ module Linguist
       lines.grep(/\S/).size
     end
 
-    # Internal: Compute average line length.
-    #
-    # Returns Integer.
-    def average_line_length
-      if lines.any?
-        lines.inject(0) { |n, l| n += l.length } / lines.length
-      else
-        0
-      end
-    end
-
     # Public: Is the blob a generated file?
     #
     # Generated source code is supressed in diffs and is ignored by
     # language statistics.
     #
-    # Requires Blob#data
-    #
-    # Includes:
-    # - XCode project XML files
-    # - Minified JavaScript
-    # - Compiled CoffeeScript
-    # - PEG.js-generated parsers
-    #
-    # Please add additional test coverage to
-    # `test/test_blob.rb#test_generated` if you make any changes.
+    # May load Blob#data
     #
     # Return true or false
     def generated?
-      if name == 'Gemfile.lock' || minified_javascript? || compiled_coffeescript? ||
-      xcode_project_file? || generated_net_docfile? || generated_parser?
-        true
-      else
-        false
-      end
-    end
-
-    # Internal: Is the blob an XCode project file?
-    #
-    # Generated if the file extension is an XCode project
-    # file extension.
-    #
-    # Returns true of false.
-    def xcode_project_file?
-      ['.xib', '.nib', '.storyboard', '.pbxproj', '.xcworkspacedata', '.xcuserstate'].include?(extname)
-    end
-
-    # Internal: Is the blob minified JS?
-    #
-    # Consider JS minified if the average line length is
-    # greater then 100c.
-    #
-    # Returns true or false.
-    def minified_javascript?
-      return unless extname == '.js'
-      average_line_length > 100
-    end
-
-    # Internal: Is the blob of JS a parser generated by PEG.js?
-    #
-    # Requires Blob#data
-    #
-    # PEG.js-generated parsers are not meant to be consumed by humans.
-    #
-    # Return true or false
-    def generated_parser?
-      return false unless extname == '.js'
-
-      # PEG.js-generated parsers include a comment near the top  of the file
-      # that marks them as such.
-      if lines[0..4].join('') =~ /^(?:[^\/]|\/[^\*])*\/\*(?:[^\*]|\*[^\/])*Generated by PEG.js/
-        return true
-      end
-
-      false
-    end
-
-    # Internal: Is the blob of JS generated by CoffeeScript?
-    #
-    # Requires Blob#data
-    #
-    # CoffeScript is meant to output JS that would be difficult to
-    # tell if it was generated or not. Look for a number of patterns
-    # output by the CS compiler.
-    #
-    # Return true or false
-    def compiled_coffeescript?
-      return false unless extname == '.js'
-
-      # CoffeeScript generated by > 1.2 include a comment on the first line
-      if lines[0] =~ /^\/\/ Generated by /
-        return true
-      end
-
-      if lines[0] == '(function() {' &&     # First line is module closure opening
-          lines[-2] == '}).call(this);' &&  # Second to last line closes module closure
-          lines[-1] == ''                   # Last line is blank
-
-        score = 0
-
-        lines.each do |line|
-          if line =~ /var /
-            # Underscored temp vars are likely to be Coffee
-            score += 1 * line.gsub(/(_fn|_i|_len|_ref|_results)/).count
-
-            # bind and extend functions are very Coffee specific
-            score += 3 * line.gsub(/(__bind|__extends|__hasProp|__indexOf|__slice)/).count
-          end
-        end
-
-        # Require a score of 3. This is fairly arbitrary. Consider
-        # tweaking later.
-        score >= 3
-      else
-        false
-      end
-    end
-
-    # Internal: Is this a generated documentation file for a .NET assembly?
-    #
-    # Requires Blob#data
-    #
-    # .NET developers often check in the XML Intellisense file along with an
-    # assembly - however, these don't have a special extension, so we have to
-    # dig into the contents to determine if it's a docfile. Luckily, these files
-    # are extremely structured, so recognizing them is easy.
-    #
-    # Returns true or false
-    def generated_net_docfile?
-      return false unless extname.downcase == ".xml"
-      return false unless lines.count > 3
-
-      # .NET Docfiles always open with <doc> and their first tag is an
-      # <assembly> tag
-      return lines[1].include?("<doc>") &&
-        lines[2].include?("<assembly>") &&
-        lines[-2].include?("</doc>")
+      @_generated ||= Generated.generated?(name, lambda { data })
     end
 
     # Public: Should the blob be indexed for searching?
@@ -389,6 +252,8 @@ module Linguist
     def indexable?
       if binary?
         false
+      elsif extname == '.txt'
+        true
       elsif language.nil?
         false
       elsif !language.searchable?
@@ -408,33 +273,15 @@ module Linguist
     #
     # Returns a Language or nil if none is detected
     def language
-      if defined? @language
-        @language
+      return @language if defined? @language
+
+      if defined?(@data) && @data.is_a?(String)
+        data = @data
       else
-        @language = guess_language
+        data = lambda { binary_mime_type? ? "" : self.data }
       end
-    end
 
-    # Internal: Guess language
-    #
-    # Please add additional test coverage to
-    # `test/test_blob.rb#test_language` if you make any changes.
-    #
-    # Returns a Language or nil
-    def guess_language
-      return if binary_mime_type?
-
-      # Disambiguate between multiple language extensions
-      disambiguate_extension_language ||
-
-        # See if there is a Language for the extension
-        pathname.language ||
-
-        # Look for idioms in first line
-        first_line_language ||
-
-        # Try to detect Language from shebang line
-        shebang_language
+      @language = Language.detect(name.to_s, data, mode)
     end
 
     # Internal: Get the lexer of the blob.
@@ -444,247 +291,6 @@ module Linguist
       language ? language.lexer : Pygments::Lexer.find_by_name('Text only')
     end
 
-    # Internal: Disambiguates between multiple language extensions.
-    #
-    # Delegates to "guess_EXTENSION_language".
-    #
-    # Please add additional test coverage to
-    # `test/test_blob.rb#test_language` if you add another method.
-    #
-    # Returns a Language or nil.
-    def disambiguate_extension_language
-      if Language.ambiguous?(extname)
-        # name = "guess_#{extname.sub(/^\./, '')}_language"
-        # send(name) if respond_to?(name)
-
-        possible_languages = Language.all.select { |l| l.extensions.include?(extname) }
-        if possible_languages.any?
-          if result = Classifier.instance.classify(data, possible_languages).first
-            result[0]
-          end
-        end
-      end
-    end
-
-    # Internal: Guess language of .cls files
-    #
-    # Returns a Language.
-    def guess_cls_language
-      if lines.grep(/^(%|\\)/).any?
-        Language['TeX']
-      elsif lines.grep(/^\s*(CLASS|METHOD|INTERFACE).*:\s*/i).any? || lines.grep(/^\s*(USING|DEFINE)/i).any?
-        Language['OpenEdge ABL']
-      elsif lines.grep(/\{$/).any? || lines.grep(/\}$/).any?
-        Language['Apex']
-      elsif lines.grep(/^(\'\*|Attribute|Option|Sub|Private|Protected|Public|Friend)/i).any?
-        Language['Visual Basic']
-      else
-        # The most common language should be the fallback
-        Language['TeX']
-      end
-    end
-
-    # Internal: Guess language of header files (.h).
-    #
-    # Returns a Language.
-    def guess_h_language
-      if lines.grep(/^@(interface|property|private|public|end)/).any?
-        Language['Objective-C']
-      elsif lines.grep(/^class |^\s+(public|protected|private):/).any?
-        Language['C++']
-      else
-        Language['C']
-      end
-    end
-
-    # Internal: Guess language of .m files.
-    #
-    # Objective-C heuristics:
-    # * Keywords  ("#import", "#include", "#ifdef", #define, "@end") or "//" and opening "\*" comments
-    #
-    # Matlab heuristics:
-    # * Leading "function " of "classdef " keyword
-    # * "%" comments
-    #
-    # Note: All "#" keywords, e.g., "#import", are guaranteed to be Objective-C. Because the ampersand
-    # is used to created function handles and anonymous functions in Matlab, most "@" keywords are not
-    # safe heuristics. However, "end" is a reserved term in Matlab and can't be used to create a valid
-    # function handle. Because @end is required to close any @implementation, @property, @interface,
-    # @synthesize, etc. directive in Objective-C, only @end needs to be checked for.
-    #
-    # Returns a Language.
-    def guess_m_language
-      # Objective-C keywords or comments
-      if lines.grep(/^#(import|include|ifdef|define)|@end/).any? || lines.grep(/^\s*\/\//).any? || lines.grep(/^\s*\/\*/).any?
-        Language['Objective-C']
-
-      # Matlab file function or class or comments
-      elsif lines.any? && lines.first.match(/^\s*(function |classdef )/) || lines.grep(/^\s*%/).any?
-        Language['Matlab']
-
-      # Fallback to Objective-C, don't want any Matlab false positives
-      else
-        Language['Objective-C']
-      end
-    end
-
-    # Internal: Guess language of .pl files
-    #
-    # The rules for disambiguation are:
-    #
-    # 1. Many perl files begin with a shebang
-    # 2. Most Prolog source files have a rule somewhere (marked by the :- operator)
-    # 3. Default to Perl, because it is more popular
-    #
-    # Returns a Language.
-    def guess_pl_language
-      if shebang_script == 'perl'
-        Language['Perl']
-      elsif lines.grep(/:-/).any?
-        Language['Prolog']
-      else
-        Language['Perl']
-      end
-    end
-
-    # Internal: Guess language of .r files.
-    #
-    # Returns a Language.
-    def guess_r_language
-      if lines.grep(/(rebol|(:\s+func|make\s+object!|^\s*context)\s*\[)/i).any?
-        Language['Rebol']
-      else
-        Language['R']
-      end
-    end
-
-    # Internal: Guess language of .t files.
-    #
-    # Returns a Language.
-    def guess_t_language
-      score = 0
-      score += 1 if lines.grep(/^% /).any?
-      score += data.gsub(/ := /).count
-      score += data.gsub(/proc |procedure |fcn |function /).count
-      score += data.gsub(/var \w+: \w+/).count
-
-      # Tell-tale signs its gotta be Perl
-      if lines.grep(/^(my )?(sub |\$|@|%)\w+/).any?
-        score = 0
-      end
-
-      if score >= 3
-        Language['Turing']
-      else
-        Language['Perl']
-      end
-    end
-
-    # Internal: Guess language of .v files.
-    #
-    # Returns a Language
-    def guess_v_language
-      if lines.grep(/^(\/\*|\/\/|module|parameter|input|output|wire|reg|always|initial|begin|\`)/).any?
-        Language['Verilog']
-      else
-        Language['Coq']
-      end
-    end
-
-    # Internal: Guess language of .gsp files.
-    #
-    # Returns a Language.
-    def guess_gsp_language
-      if lines.grep(/<%|<%@|\$\{|<%|<g:|<meta name="layout"|<r:/).any?
-        Language['Groovy Server Pages']
-      else
-        Language['Gosu']
-      end
-    end
-
-    # Internal: Guess language from the first line.
-    #
-    # Look for leading "<?php" in Drupal files
-    #
-    # Returns a Language.
-    def first_line_language
-      # Only check files with drupal php extensions
-      return unless drupal_extname?
-
-      # Fail fast if blob isn't viewable?
-      return unless viewable?
-
-      if lines.first.to_s =~ /^<\?php/
-        Language['PHP']
-      end
-    end
-
-    # Internal: Extract the script name from the shebang line
-    #
-    # Requires Blob#data
-    #
-    # Examples
-    #
-    #   '#!/usr/bin/ruby'
-    #   # => 'ruby'
-    #
-    #   '#!/usr/bin/env ruby'
-    #   # => 'ruby'
-    #
-    #   '#!/usr/bash/python2.4'
-    #   # => 'python'
-    #
-    # Please add additional test coverage to
-    # `test/test_blob.rb#test_shebang_script` if you make any changes.
-    #
-    # Returns a script name String or nil
-    def shebang_script
-      # Fail fast if blob isn't viewable?
-      return unless viewable?
-
-      if lines.any? && (match = lines[0].match(/(.+)\n?/)) && (bang = match[0]) =~ /^#!/
-        bang.sub!(/^#! /, '#!')
-        tokens = bang.split(' ')
-        pieces = tokens.first.split('/')
-        if pieces.size > 1
-          script = pieces.last
-        else
-          script = pieces.first.sub('#!', '')
-        end
-
-        script = script == 'env' ? tokens[1] : script
-
-        # python2.4 => python
-        if script =~ /((?:\d+\.?)+)/
-          script.sub! $1, ''
-        end
-
-        # Check for multiline shebang hacks that exec themselves
-        #
-        #   #!/bin/sh
-        #   exec foo "$0" "$@"
-        #
-        if script == 'sh' &&
-            lines[0...5].any? { |l| l.match(/exec (\w+).+\$0.+\$@/) }
-          script = $1
-        end
-
-        script
-      end
-    end
-
-    # Internal: Get Language for shebang script
-    #
-    # Returns the Language or nil
-    def shebang_language
-      # Skip file extensions unlikely to have shebangs
-      return unless shebang_extname?
-
-      if script = shebang_script
-        Language[script]
-      end
-    end
-
     # Public: Highlight syntax of blob
     #
     # options - A Hash of options (defaults to {})
@@ -710,12 +316,5 @@ module Linguist
         ''
       end
     end
-
-    Language.overridden_extensions.each do |extension|
-      name = "guess_#{extension.sub(/^\./, '')}_language".to_sym
-      unless instance_methods.map(&:to_sym).include?(name)
-        raise NotImplementedError, "Language##{name} was not defined"
-      end
-    end
   end
 end

lib/linguist/classifier.rb

@@ -1,112 +1,88 @@
-require 'linguist/language'
 require 'linguist/tokenizer'
 
 module Linguist
   # Language bayesian classifier.
   class Classifier
-    # Internal: Path to persisted classifier db.
-    PATH = File.expand_path('../classifier.yml', __FILE__)
-
-    # Public: Check if persisted db exists on disk.
-    #
-    # Returns Boolean.
-    def self.exist?
-      File.exist?(PATH)
-    end
-
-    # Public: Get persisted Classifier instance.
-    #
-    # Returns Classifier.
-    def self.instance
-      @instance ||= YAML.load_file(PATH)
-    end
-
-    # Public: Initialize a Classifier.
-    def initialize
-      @tokens_total    = 0
-      @languages_total = 0
-      @tokens          = Hash.new { |h, k| h[k] = Hash.new(0) }
-      @language_tokens = Hash.new(0)
-      @languages       = Hash.new(0)
-    end
-
-    # Public: Compare Classifier objects.
-    #
-    # other - Classifier object to compare to.
-    #
-    # Returns Boolean.
-    def eql?(other)
-      # Lazy fast check counts only
-      other.is_a?(self.class) &&
-        @tokens_total == other.instance_variable_get(:@tokens_total) &&
-        @languages_total == other.instance_variable_get(:@languages_total)
-    end
-    alias_method :==, :eql?
-
     # Public: Train classifier that data is a certain language.
     #
-    # language - Language of data
+    # db       - Hash classifier database object
+    # language - String language of data
     # data     - String contents of file
     #
     # Examples
     #
-    #   train(Language['Ruby'], "def hello; end")
+    #   Classifier.train(db, 'Ruby', "def hello; end")
     #
     # Returns nothing.
-    def train(language, data)
-      language = language.name
-      tokens   = Tokenizer.new(data).tokens
+    def self.train!(db, language, data)
+      tokens = Tokenizer.tokenize(data)
+
+      db['tokens_total'] ||= 0
+      db['languages_total'] ||= 0
+      db['tokens'] ||= {}
+      db['language_tokens'] ||= {}
+      db['languages'] ||= {}
 
       tokens.each do |token|
-        @tokens[language][token] += 1
-        @language_tokens[language] += 1
-        @tokens_total += 1
+        db['tokens'][language] ||= {}
+        db['tokens'][language][token] ||= 0
+        db['tokens'][language][token] += 1
+        db['language_tokens'][language] ||= 0
+        db['language_tokens'][language] += 1
+        db['tokens_total'] += 1
       end
-      @languages[language] += 1
-      @languages_total += 1
+      db['languages'][language] ||= 0
+      db['languages'][language] += 1
+      db['languages_total'] += 1
 
       nil
     end
 
-    # Public: Verify internal counts are consistent.
-    #
-    # Returns Boolean.
-    def verify
-      @languages.inject(0) { |n, (l, c)| n += c } == @languages_total &&
-        @language_tokens.inject(0) { |n, (l, c)| n += c } == @tokens_total &&
-        @tokens.inject(0) { |n, (l, ts)| n += ts.inject(0) { |m, (t, c)| m += c } } == @tokens_total
-    end
-
-    # Public: Prune infrequent tokens.
-    #
-    # Returns receiver Classifier instance.
-    def gc
-      self
-    end
-
     # Public: Guess language of data.
     #
+    # db        - Hash of classifer tokens database.
     # data      - Array of tokens or String data to analyze.
-    # languages - Array of Languages to restrict to.
+    # languages - Array of language name Strings to restrict to.
     #
     # Examples
     #
-    #   classify("def hello; end")
-    #   # => [ [Language['Ruby'], 0.90], [Language['Python'], 0.2], ... ]
+    #   Classifier.classify(db, "def hello; end")
+    #   # => [ 'Ruby', 0.90], ['Python', 0.2], ... ]
     #
     # Returns sorted Array of result pairs. Each pair contains the
-    # Language and a Float score.
-    def classify(tokens, languages = @languages.keys)
-      tokens = Tokenizer.new(tokens).tokens if tokens.is_a?(String)
+    # String language name and a Float score.
+    def self.classify(db, tokens, languages = nil)
+      languages ||= db['languages'].keys
+      new(db).classify(tokens, languages)
+    end
+
+    # Internal: Initialize a Classifier.
+    def initialize(db = {})
+      @tokens_total    = db['tokens_total']
+      @languages_total = db['languages_total']
+      @tokens          = db['tokens']
+      @language_tokens = db['language_tokens']
+      @languages       = db['languages']
+    end
+
+    # Internal: Guess language of data
+    #
+    # data      - Array of tokens or String data to analyze.
+    # languages - Array of language name Strings to restrict to.
+    #
+    # Returns sorted Array of result pairs. Each pair contains the
+    # String language name and a Float score.
+    def classify(tokens, languages)
+      return [] if tokens.nil?
+      tokens = Tokenizer.tokenize(tokens) if tokens.is_a?(String)
 
       scores = {}
       languages.each do |language|
-        language_name = language.is_a?(Language) ? language.name : language
-        scores[language_name] = tokens_probability(tokens, language_name) +
-                                   language_probability(language_name)
+        scores[language] = tokens_probability(tokens, language) +
+                                   language_probability(language)
       end
 
-      scores.sort { |a, b| b[1] <=> a[1] }.map { |score| [Language[score[0]], score[1]] }
+      scores.sort { |a, b| b[1] <=> a[1] }.map { |score| [score[0], score[1]] }
     end
 
     # Internal: Probably of set of tokens in a language occuring - P(D | C)
@@ -143,41 +119,5 @@ module Linguist
     def language_probability(language)
       Math.log(@languages[language].to_f / @languages_total.to_f)
     end
-
-    # Public: Serialize classifier to YAML.
-    #
-    # opts - Hash of YAML options.
-    #
-    # Returns nothing.
-    def to_yaml(io)
-      data = "--- !ruby/object:Linguist::Classifier\n"
-
-      data << "languages_total: #{@languages_total}\n"
-      data << "tokens_total: #{@tokens_total}\n"
-
-      data << "languages:\n"
-      @languages.sort.each do |language, count|
-        data << "  #{{language => count}.to_yaml.lines.to_a[1]}"
-      end
-
-      data << "language_tokens:\n"
-      @language_tokens.sort.each do |language, count|
-        data << "  #{{language => count}.to_yaml.lines.to_a[1]}"
-      end
-
-      data << "tokens:\n"
-      @tokens.sort.each do |language, tokens|
-        data << "  #{{language => true}.to_yaml.lines.to_a[1].sub(/ true/, "")}"
-        tokens.sort.each do |token, count|
-          data << "    #{{token => count}.to_yaml.lines.to_a[1]}"
-        end
-      end
-
-      io.write data
-      nil
-    end
   end
-
-  # Eager load instance
-  Classifier.instance if Classifier.exist?
 end

lib/linguist/generated.rb

@@ -0,0 +1,162 @@
+module Linguist
+  class Generated
+    # Public: Is the blob a generated file?
+    #
+    # name - String filename
+    # data - String blob data. A block also maybe passed in for lazy
+    #        loading. This behavior is deprecated and you should always
+    #        pass in a String.
+    #
+    # Return true or false
+    def self.generated?(name, data)
+      new(name, data).generated?
+    end
+
+    # Internal: Initialize Generated instance
+    #
+    # name - String filename
+    # data - String blob data
+    def initialize(name, data)
+      @name = name
+      @extname = File.extname(name)
+      @_data = data
+    end
+
+    attr_reader :name, :extname
+
+    # Lazy load blob data if block was passed in.
+    #
+    # Awful, awful stuff happening here.
+    #
+    # Returns String data.
+    def data
+      @data ||= @_data.respond_to?(:call) ? @_data.call() : @_data
+    end
+
+    # Public: Get each line of data
+    #
+    # Returns an Array of lines
+    def lines
+      # TODO: data should be required to be a String, no nils
+      @lines ||= data ? data.split("\n", -1) : []
+    end
+
+    # Internal: Is the blob a generated file?
+    #
+    # Generated source code is supressed in diffs and is ignored by
+    # language statistics.
+    #
+    # Please add additional test coverage to
+    # `test/test_blob.rb#test_generated` if you make any changes.
+    #
+    # Return true or false
+    def generated?
+      name == 'Gemfile.lock' ||
+        minified_javascript? ||
+        compiled_coffeescript? ||
+        xcode_project_file? ||
+        generated_net_docfile? ||
+        generated_parser?
+    end
+
+    # Internal: Is the blob an XCode project file?
+    #
+    # Generated if the file extension is an XCode project
+    # file extension.
+    #
+    # Returns true of false.
+    def xcode_project_file?
+      ['.xib', '.nib', '.storyboard', '.pbxproj', '.xcworkspacedata', '.xcuserstate'].include?(extname)
+    end
+
+    # Internal: Is the blob minified JS?
+    #
+    # Consider JS minified if the average line length is
+    # greater then 100c.
+    #
+    # Returns true or false.
+    def minified_javascript?
+      return unless extname == '.js'
+      if lines.any?
+        (lines.inject(0) { |n, l| n += l.length } / lines.length) > 100
+      else
+        false
+      end
+    end
+
+    # Internal: Is the blob of JS generated by CoffeeScript?
+    #
+    # CoffeScript is meant to output JS that would be difficult to
+    # tell if it was generated or not. Look for a number of patterns
+    # output by the CS compiler.
+    #
+    # Return true or false
+    def compiled_coffeescript?
+      return false unless extname == '.js'
+
+      # CoffeeScript generated by > 1.2 include a comment on the first line
+      if lines[0] =~ /^\/\/ Generated by /
+        return true
+      end
+
+      if lines[0] == '(function() {' &&     # First line is module closure opening
+          lines[-2] == '}).call(this);' &&  # Second to last line closes module closure
+          lines[-1] == ''                   # Last line is blank
+
+        score = 0
+
+        lines.each do |line|
+          if line =~ /var /
+            # Underscored temp vars are likely to be Coffee
+            score += 1 * line.gsub(/(_fn|_i|_len|_ref|_results)/).count
+
+            # bind and extend functions are very Coffee specific
+            score += 3 * line.gsub(/(__bind|__extends|__hasProp|__indexOf|__slice)/).count
+          end
+        end
+
+        # Require a score of 3. This is fairly arbitrary. Consider
+        # tweaking later.
+        score >= 3
+      else
+        false
+      end
+    end
+
+    # Internal: Is this a generated documentation file for a .NET assembly?
+    #
+    # .NET developers often check in the XML Intellisense file along with an
+    # assembly - however, these don't have a special extension, so we have to
+    # dig into the contents to determine if it's a docfile. Luckily, these files
+    # are extremely structured, so recognizing them is easy.
+    #
+    # Returns true or false
+    def generated_net_docfile?
+      return false unless extname.downcase == ".xml"
+      return false unless lines.count > 3
+
+      # .NET Docfiles always open with <doc> and their first tag is an
+      # <assembly> tag
+      return lines[1].include?("<doc>") &&
+        lines[2].include?("<assembly>") &&
+        lines[-2].include?("</doc>")
+    end
+
+    # Internal: Is the blob of JS a parser generated by PEG.js?
+    #
+    # PEG.js-generated parsers are not meant to be consumed by humans.
+    #
+    # Return true or false
+    def generated_parser?
+      return false unless extname == '.js'
+
+      # PEG.js-generated parsers include a comment near the top  of the file
+      # that marks them as such.
+      if lines[0..4].join('') =~ /^(?:[^\/]|\/[^\*])*\/\*(?:[^\*]|\*[^\/])*Generated by PEG.js/
+        return true
+      end
+
+      false
+    end
+  end
+end

lib/linguist/language.rb

@@ -2,6 +2,9 @@ require 'escape_utils'
 require 'pygments'
 require 'yaml'
 
+require 'linguist/classifier'
+require 'linguist/samples'
+
 module Linguist
   # Language names that are recognizable by GitHub. Defined languages
   # can be highlighted, searched and listed under the Top Languages page.
@@ -9,30 +12,15 @@ module Linguist
   # Languages are defined in `lib/linguist/languages.yml`.
   class Language
     @languages       = []
-    @overrides       = {}
     @index           = {}
     @name_index      = {}
     @alias_index     = {}
-    @extension_index = {}
-    @filename_index  = {}
+    @extension_index = Hash.new { |h,k| h[k] = [] }
+    @filename_index  = Hash.new { |h,k| h[k] = [] }
 
     # Valid Languages types
     TYPES = [:data, :markup, :programming]
 
-    # Internal: Test if extension maps to multiple Languages.
-    #
-    # Returns true or false.
-    def self.ambiguous?(extension)
-      @overrides.include?(extension)
-    end
-
-    # Internal: Return overridden extensions.
-    #
-    # Returns extensions Array.
-    def self.overridden_extensions
-      @overrides.keys
-    end
-
     # Internal: Create a new Language object
     #
     # attributes - A hash of attributes
@@ -65,34 +53,45 @@ module Linguist
           raise ArgumentError, "Extension is missing a '.': #{extension.inspect}"
         end
 
-        unless ambiguous?(extension)
-          # Index the extension with a leading ".": ".rb"
-          @extension_index[extension] = language
-
-          # Index the extension without a leading ".": "rb"
-          @extension_index[extension.sub(/^\./, '')] = language
-        end
-      end
-
-      language.overrides.each do |extension|
-        if extension !~ /^\./
-          raise ArgumentError, "Extension is missing a '.': #{extension.inspect}"
-        end
-
-        if l = @overrides[extension]
-          raise ArgumentError, "#{extension} is already overridden by #{l.name}"
-        end
-
-        @overrides[extension] = language
+        @extension_index[extension] << language
       end
 
       language.filenames.each do |filename|
-        @filename_index[filename] = language
+        @filename_index[filename] << language
       end
 
       language
     end
 
+    # Public: Detects the Language of the blob.
+    #
+    # name - String filename
+    # data - String blob data. A block also maybe passed in for lazy
+    #        loading. This behavior is deprecated and you should always
+    #        pass in a String.
+    # mode - Optional String mode (defaults to nil)
+    #
+    # Returns Language or nil.
+    def self.detect(name, data, mode = nil)
+      # A bit of an elegant hack. If the file is exectable but extensionless,
+      # append a "magic" extension so it can be classified with other
+      # languages that have shebang scripts.
+      if File.extname(name).empty? && mode && (mode.to_i(8) & 05) == 05
+        name += ".script!"
+      end
+
+      possible_languages = find_by_filename(name)
+
+      if possible_languages.length > 1
+        data = data.call() if data.respond_to?(:call)
+        if result = Classifier.classify(Samples::DATA, data, possible_languages.map(&:name)).first
+          Language[result[0]]
+        end
+      else
+        possible_languages.first
+      end
+    end
+
     # Public: Get all Languages
     #
     # Returns an Array of Languages
@@ -128,33 +127,19 @@ module Linguist
       @alias_index[name]
     end
 
-    # Public: Look up Language by extension.
-    #
-    # extension - The extension String. May include leading "."
-    #
-    # Examples
-    #
-    #   Language.find_by_extension('.rb')
-    #   # => #<Language name="Ruby">
-    #
-    # Returns the Language or nil if none was found.
-    def self.find_by_extension(extension)
-      @extension_index[extension]
-    end
-
-    # Public: Look up Language by filename.
+    # Public: Look up Languages by filename.
     #
     # filename - The path String.
     #
     # Examples
     #
     #   Language.find_by_filename('foo.rb')
-    #   # => #<Language name="Ruby">
+    #   # => [#<Language name="Ruby">]
     #
-    # Returns the Language or nil if none was found.
+    # Returns all matching Languages or [] if none were found.
     def self.find_by_filename(filename)
       basename, extname = File.basename(filename), File.extname(filename)
-      @filename_index[basename] || @extension_index[extname]
+      @filename_index[basename] + @extension_index[extname]
     end
 
     # Public: Look up Language by its name or lexer.
@@ -241,10 +226,11 @@ module Linguist
 
       # Set extensions or default to [].
       @extensions = attributes[:extensions] || []
-      @overrides  = attributes[:overrides]  || []
       @filenames  = attributes[:filenames]  || []
 
-      @primary_extension = attributes[:primary_extension] || default_primary_extension || extensions.first
+      unless @primary_extension = attributes[:primary_extension]
+        raise ArgumentError, "#{@name} is missing primary extension"
+      end
 
       # Prepend primary extension unless its already included
       if primary_extension && !extensions.include?(primary_extension)
@@ -347,11 +333,6 @@ module Linguist
     # Returns the extension String.
     attr_reader :primary_extension
 
-    # Internal: Get overridden extensions.
-    #
-    # Returns the extensions Array.
-    attr_reader :overrides
-
     # Public: Get filenames
     #
     # Examples
@@ -381,13 +362,6 @@ module Linguist
       name.downcase.gsub(/\s/, '-')
     end
 
-    # Internal: Get default primary extension.
-    #
-    # Returns the extension String.
-    def default_primary_extension
-      extensions.first
-    end
-
     # Public: Get Language group
     #
     # Returns a Language
@@ -451,9 +425,34 @@ module Linguist
     end
   end
 
+  extensions = Samples::DATA['extnames']
+  filenames = Samples::DATA['filenames']
   popular = YAML.load_file(File.expand_path("../popular.yml", __FILE__))
 
   YAML.load_file(File.expand_path("../languages.yml", __FILE__)).each do |name, options|
+    options['extensions'] ||= []
+    options['filenames'] ||= []
+
+    if extnames = extensions[name]
+      extnames.each do |extname|
+        if !options['extensions'].include?(extname)
+          options['extensions'] << extname
+        else
+          warn "#{name} #{extname.inspect} is already defined in samples/. Remove from languages.yml."
+        end
+      end
+    end
+
+    if fns = filenames[name]
+      fns.each do |filename|
+        if !options['filenames'].include?(filename)
+          options['filenames'] << filename
+        else
+          warn "#{name} #{filename.inspect} is already defined in samples/. Remove from languages.yml."
+        end
+      end
+    end
+
     Language.create(
       :name              => name,
       :color             => options['color'],
@@ -464,9 +463,8 @@ module Linguist
       :group_name        => options['group'],
       :searchable        => options.key?('searchable') ? options['searchable'] : true,
       :search_term       => options['search_term'],
-      :extensions        => options['extensions'],
+      :extensions        => options['extensions'].sort,
       :primary_extension => options['primary_extension'],
-      :overrides         => options['overrides'],
       :filenames         => options['filenames'],
       :popular           => popular.include?(name)
     )

lib/linguist/md5.rb

@@ -0,0 +1,38 @@
+require 'digest/md5'
+
+module Linguist
+  module MD5
+    # Public: Create deep nested digest of value object.
+    #
+    # Useful for object comparsion.
+    #
+    # obj - Object to digest.
+    #
+    # Returns String hex digest
+    def self.hexdigest(obj)
+      digest = Digest::MD5.new
+
+      case obj
+      when String, Symbol, Integer
+        digest.update "#{obj.class}"
+        digest.update "#{obj}"
+      when TrueClass, FalseClass, NilClass
+        digest.update "#{obj.class}"
+      when Array
+        digest.update "#{obj.class}"
+        for e in obj
+          digest.update(hexdigest(e))
+        end
+      when Hash
+        digest.update "#{obj.class}"
+        for e in obj.map { |(k, v)| hexdigest([k, v]) }.sort
+          digest.update(e)
+        end
+      else
+        raise TypeError, "can't convert #{obj.inspect} into String"
+      end
+
+      digest.hexdigest
+    end
+  end
+end

lib/linguist/mime.rb

@@ -1,91 +0,0 @@
-require 'mime/types'
-require 'yaml'
-
-class MIME::Type
-  attr_accessor :override
-end
-
-# Register additional mime type extensions
-#
-# Follows same format as mime-types data file
-#   https://github.com/halostatue/mime-types/blob/master/lib/mime/types.rb.data
-File.read(File.expand_path("../mimes.yml", __FILE__)).lines.each do |line|
-  # Regexp was cargo culted from mime-types lib
-  next unless line =~ %r{^
-    #{MIME::Type::MEDIA_TYPE_RE}
-    (?:\s@([^\s]+))?
-    (?:\s:(#{MIME::Type::ENCODING_RE}))?
-  }x
-
-  mediatype  = $1
-  subtype    = $2
-  extensions = $3
-  encoding   = $4
-
-  # Lookup existing mime type
-  mime_type = MIME::Types["#{mediatype}/#{subtype}"].first ||
-    # Or create a new instance
-    MIME::Type.new("#{mediatype}/#{subtype}")
-
-  if extensions
-    extensions.split(/,/).each do |extension|
-      mime_type.extensions << extension
-    end
-  end
-
-  if encoding
-    mime_type.encoding = encoding
-  end
-
-  mime_type.override = true
-
-  # Kind of hacky, but we need to reindex the mime type after making changes
-  MIME::Types.add_type_variant(mime_type)
-  MIME::Types.index_extensions(mime_type)
-end
-
-module Linguist
-  module Mime
-    # Internal: Look up mime type for extension.
-    #
-    # ext - The extension String. May include leading "."
-    #
-    # Examples
-    #
-    #   Mime.mime_for('.html')
-    #   # => 'text/html'
-    #
-    #   Mime.mime_for('txt')
-    #   # => 'text/plain'
-    #
-    # Return mime type String otherwise falls back to 'text/plain'.
-    def self.mime_for(ext)
-      mime_type = lookup_mime_type_for(ext)
-      mime_type ? mime_type.to_s : 'text/plain'
-    end
-
-    # Internal: Lookup mime type for extension or mime type
-    #
-    # ext_or_mime_type - A file extension ".txt" or mime type "text/plain".
-    #
-    # Returns a MIME::Type
-    def self.lookup_mime_type_for(ext_or_mime_type)
-      ext_or_mime_type ||= ''
-
-      if ext_or_mime_type =~ /\w+\/\w+/
-        guesses = ::MIME::Types[ext_or_mime_type]
-      else
-        guesses = ::MIME::Types.type_for(ext_or_mime_type)
-      end
-
-      # Use custom override first
-      guesses.detect { |type| type.override } ||
-
-        # Prefer text mime types over binary
-        guesses.detect { |type| type.ascii? } ||
-
-        # Otherwise use the first guess
-        guesses.first
-    end
-  end
-end

lib/linguist/mimes.yml

@@ -1,62 +0,0 @@
-# Additional types to add to MIME::Types
-#
-# MIME types are used to set the Content-Type of raw binary blobs. All text
-# blobs are served as text/plain regardless of their type to ensure they
-# open in the browser rather than downloading.
-#
-# The encoding helps determine whether a file should be treated as plain
-# text or binary. By default, a mime type's encoding is base64 (binary).
-# These types will show a "View Raw" link. To force a type to render as
-# plain text, set it to 8bit for UTF-8. text/* types will be treated as
-# text by default.
-#
-#   <type> @<extensions> :<encoding>
-#
-# type       - mediatype/subtype
-# extensions - comma seperated extension list
-# encoding   - base64 (binary), 7bit (ASCII), 8bit (UTF-8), or
-#              quoted-printable (Printable ASCII).
-#
-# Follows same format as mime-types data file
-#   https://github.com/halostatue/mime-types/blob/master/lib/mime/types.rb.data
-#
-# Any additions or modifications (even trivial) should have corresponding
-# test change in `test/test_mime.rb`.
-
-# TODO: Lookup actual types
-application/octet-stream @a,blend,gem,graffle,ipa,lib,mcz,nib,o,ogv,otf,pfx,pigx,plgx,psd,sib,spl,sqlite3,swc,ucode,xpi
-
-# Please keep this list alphabetized
-application/java-archive @ear,war
-application/netcdf :8bit
-application/ogg @ogg
-application/postscript :base64
-application/vnd.adobe.air-application-installer-package+zip @air
-application/vnd.mozilla.xul+xml :8bit
-application/vnd.oasis.opendocument.presentation @odp
-application/vnd.oasis.opendocument.spreadsheet @ods
-application/vnd.oasis.opendocument.text @odt
-application/vnd.openofficeorg.extension @oxt
-application/vnd.openxmlformats-officedocument.presentationml.presentation @pptx
-application/x-chrome-extension @crx
-application/x-iwork-keynote-sffkey @key
-application/x-iwork-numbers-sffnumbers @numbers
-application/x-iwork-pages-sffpages @pages
-application/x-ms-xbap @xbap :8bit
-application/x-parrot-bytecode @pbc
-application/x-shockwave-flash @swf
-application/x-silverlight-app @xap
-application/x-supercollider @sc :8bit
-application/x-troff-ms :8bit
-application/x-wais-source :8bit
-application/xaml+xml @xaml :8bit
-application/xslt+xml @xslt :8bit
-image/x-icns @icns
-text/cache-manifest @manifest
-text/plain @cu,cxx
-text/x-logtalk @lgt
-text/x-nemerle @n
-text/x-nimrod @nim
-text/x-ocaml @ml,mli,mll,mly,sig,sml
-text/x-rust @rs,rc
-text/x-scheme @rkt,scm,sls,sps,ss

lib/linguist/pathname.rb

@@ -1,92 +0,0 @@
-require 'linguist/language'
-require 'linguist/mime'
-require 'pygments'
-
-module Linguist
-  # Similar to ::Pathname, Linguist::Pathname wraps a path string and
-  # provides helpful query methods. Its useful when you only have a
-  # filename but not a blob and need to figure out the language of the file.
-  class Pathname
-    # Public: Initialize a Pathname
-    #
-    # path - A filename String. The file may or maybe actually exist.
-    #
-    # Returns a Pathname.
-    def initialize(path)
-      @path = path
-    end
-
-    # Public: Get the basename of the path
-    #
-    # Examples
-    #
-    #   Pathname.new('sub/dir/file.rb').basename
-    #   # => 'file.rb'
-    #
-    # Returns a String.
-    def basename
-      File.basename(@path)
-    end
-
-    # Public: Get the extname of the path
-    #
-    # Examples
-    #
-    #   Pathname.new('.rb').extname
-    #   # => '.rb'
-    #
-    #   Pathname.new('file.rb').extname
-    #   # => '.rb'
-    #
-    # Returns a String.
-    def extname
-      File.extname(@path)
-    end
-
-    # Public: Get the language of the path
-    #
-    # The path extension name is the only heuristic used to detect the
-    # language name.
-    #
-    # Examples
-    #
-    #   Pathname.new('file.rb').language
-    #   # => Language['Ruby']
-    #
-    # Returns a Language or nil if none was found.
-    def language
-      @language ||= Language.find_by_filename(@path)
-    end
-
-    # Internal: Get the lexer of the path
-    #
-    # Returns a Lexer.
-    def lexer
-      language ? language.lexer : Pygments::Lexer.find_by_name('Text only')
-    end
-
-    # Public: Get the mime type
-    #
-    # Examples
-    #
-    #   Pathname.new('index.html').mime_type
-    #   # => 'text/html'
-    #
-    # Returns a mime type String.
-    def mime_type
-      @mime_type ||= Mime.mime_for(extname)
-    end
-
-    # Public: Return self as String
-    #
-    # Returns a String
-    def to_s
-      @path.dup
-    end
-
-    def eql?(other)
-      other.is_a?(self.class) && @path == other.to_s
-    end
-    alias_method :==, :eql?
-  end
-end

lib/linguist/repository.rb

@@ -80,7 +80,7 @@ module Linguist
       end
 
       # Compute total size
-      @size = @sizes.inject(0) { |s,(k,v)| s + v }
+      @size = @sizes.inject(0) { |s,(_,v)| s + v }
 
       # Get primary language
       if primary = @sizes.max_by { |(_, size)| size }

lib/linguist/sample.rb

@@ -1,74 +0,0 @@
-require 'linguist/classifier'
-require 'linguist/language'
-
-module Linguist
-  # Model for accessing classifier training data.
-  class Sample
-    # Samples live in test/ for now, we'll eventually move them out
-    PATH = File.expand_path("../../../test/fixtures", __FILE__)
-
-    # Public: Iterate over each Sample.
-    #
-    # &block - Yields Sample to block
-    #
-    # Returns nothing.
-    def self.each(&block)
-      Dir.entries(PATH).each do |category|
-        next if category == '.' || category == '..'
-
-        # Skip text and binary for now
-        # Possibly reconsider this later
-        next if category == 'text' || category == 'binary'
-
-        # Map directory name to a Language alias
-        language = Linguist::Language.find_by_alias(category)
-        raise "No language for #{category.inspect}" unless language
-
-        dirname = File.join(PATH, category)
-        Dir.entries(dirname).each do |filename|
-          next if filename == '.' || filename == '..'
-          yield new(File.join(dirname, filename), language)
-        end
-      end
-
-      nil
-    end
-
-    # Public: Build Classifier from all samples.
-    #
-    # Returns trained Classifier.
-    def self.classifier
-      classifier = Classifier.new
-      each { |sample| classifier.train(sample.language, sample.data) }
-      classifier.gc
-    end
-
-    # Internal: Initialize Sample.
-    #
-    # Samples should be initialized by Sample.each.
-    #
-    # path     - String full path to file.
-    # language - Language of sample.
-    def initialize(path, language)
-      @path     = path
-      @language = language
-    end
-
-    # Public: Get full path to file.
-    #
-    # Returns String.
-    attr_reader :path
-
-    # Public: Get sample language.
-    #
-    # Returns Language.
-    attr_reader :language
-
-    # Public: Read file contents.
-    #
-    # Returns String.
-    def data
-      File.read(path)
-    end
-  end
-end

lib/linguist/samples.rb

@@ -0,0 +1,96 @@
+require 'yaml'
+
+require 'linguist/md5'
+require 'linguist/classifier'
+
+module Linguist
+  # Model for accessing classifier training data.
+  module Samples
+    # Path to samples root directory
+    ROOT = File.expand_path("../../../samples", __FILE__)
+
+    # Path for serialized samples db
+    PATH = File.expand_path('../samples.json', __FILE__)
+
+    # Hash of serialized samples object
+    if File.exist?(PATH)
+      DATA = YAML.load_file(PATH)
+    end
+
+    # Public: Iterate over each sample.
+    #
+    # &block - Yields Sample to block
+    #
+    # Returns nothing.
+    def self.each(&block)
+      Dir.entries(ROOT).each do |category|
+        next if category == '.' || category == '..'
+
+        # Skip text and binary for now
+        # Possibly reconsider this later
+        next if category == 'Text' || category == 'Binary'
+
+        dirname = File.join(ROOT, category)
+        Dir.entries(dirname).each do |filename|
+          next if filename == '.' || filename == '..'
+
+          if filename == 'filenames'
+            Dir.entries(File.join(dirname, filename)).each do |subfilename|
+              next if subfilename == '.' || subfilename == '..'
+
+              yield({
+                :path    => File.join(dirname, filename, subfilename),
+                :language => category,
+                :filename => subfilename
+              })
+            end
+          else
+            if File.extname(filename) == ""
+              raise "#{File.join(dirname, filename)} is missing an extension, maybe it belongs in filenames/ subdir"
+            end
+
+            yield({
+              :path     => File.join(dirname, filename),
+              :language => category,
+              :extname  => File.extname(filename)
+            })
+          end
+        end
+      end
+
+      nil
+    end
+
+    # Public: Build Classifier from all samples.
+    #
+    # Returns trained Classifier.
+    def self.data
+      db = {}
+      db['extnames'] = {}
+      db['filenames'] = {}
+
+      each do |sample|
+        language_name = sample[:language]
+
+        if sample[:extname]
+          db['extnames'][language_name] ||= []
+          if !db['extnames'][language_name].include?(sample[:extname])
+            db['extnames'][language_name] << sample[:extname]
+          end
+        end
+
+        if sample[:filename]
+          db['filenames'][language_name] ||= []
+          db['filenames'][language_name] << sample[:filename]
+        end
+
+        data = File.read(sample[:path])
+        Classifier.train!(db, language_name, data)
+      end
+
+      db['md5'] = Linguist::MD5.hexdigest(db)
+
+      db
+    end
+  end
+end

lib/linguist/tokenizer.rb

@@ -1,3 +1,5 @@
+require 'strscan'
+
 module Linguist
   # Generic programming language tokenizer.
   #
@@ -5,25 +7,39 @@ module Linguist
   # It strips any data strings or comments and preserves significant
   # language symbols.
   class Tokenizer
-    # Public: Initialize a Tokenizer.
+    # Public: Extract tokens from data
     #
-    # data - String data to scan.
-    def initialize(data)
-      @data = data
-    end
-
-    # Public: Get source data.
-    #
-    # Returns String.
-    attr_reader :data
-
-    # Public: Extract tokens from data.
+    # data - String to tokenize
     #
     # Returns Array of token Strings.
-    def tokens
-      extract_tokens(data)
+    def self.tokenize(data)
+      new.extract_tokens(data)
     end
 
+    # Start state on token, ignore anything till the next newline
+    SINGLE_LINE_COMMENTS = [
+      '//', # C
+      '#',  # Ruby
+      '%',  # Tex
+    ]
+
+    # Start state on opening token, ignore anything until the closing
+    # token is reached.
+    MULTI_LINE_COMMENTS = [
+      ['/*', '*/'],    # C
+      ['<!--', '-->'], # XML
+      ['{-', '-}'],    # Haskell
+      ['(*', '*)']     # Coq
+    ]
+
+    START_SINGLE_LINE_COMMENT =  Regexp.compile(SINGLE_LINE_COMMENTS.map { |c|
+      "\s*#{Regexp.escape(c)} "
+    }.join("|"))
+
+    START_MULTI_LINE_COMMENT =  Regexp.compile(MULTI_LINE_COMMENTS.map { |c|
+      Regexp.escape(c[0])
+    }.join("|"))
+
     # Internal: Extract generic tokens from data.
     #
     # data - String to scan.
@@ -39,54 +55,46 @@ module Linguist
 
       tokens = []
       until s.eos?
-        # Ruby single line comment
-        if token = s.scan(/# /)
-          tokens << "#"
+        if token = s.scan(/^#!.+$/)
+          if name = extract_shebang(token)
+            tokens << "SHEBANG#!#{name}"
+          end
+
+        # Single line comment
+        elsif s.beginning_of_line? && token = s.scan(START_SINGLE_LINE_COMMENT)
+          # tokens << token.strip
           s.skip_until(/\n|\Z/)
 
-        # C style single line comment
-        elsif token = s.scan(/\/\/ /)
-          tokens << "//"
-          s.skip_until(/\n|\Z/)
-
-        # Leading Tex or Matlab comments
-        elsif token = s.scan(/\n%/)
-          tokens << "%"
-          s.skip_until(/\n|\Z/)
-
-        # C multiline comments
-        elsif token = s.scan(/\/\*/)
-          tokens << "/*"
-          s.skip_until(/\*\//)
-          tokens << "*/"
-
-        # Haskell multiline comments
-        elsif token = s.scan(/\{-/)
-          tokens << "{-"
-          s.skip_until(/-\}/)
-          tokens << "-}"
-
-        # XML multiline comments
-        elsif token = s.scan(/<!--/)
-          tokens << "<!--"
-          s.skip_until(/-->/)
-          tokens << "-->"
+        # Multiline comments
+        elsif token = s.scan(START_MULTI_LINE_COMMENT)
+          # tokens << token
+          close_token = MULTI_LINE_COMMENTS.assoc(token)[1]
+          s.skip_until(Regexp.compile(Regexp.escape(close_token)))
+          # tokens << close_token
 
         # Skip single or double quoted strings
         elsif s.scan(/"/)
-          s.skip_until(/[^\\]"/)
+          if s.peek(1) == "\""
+            s.getch
+          else
+            s.skip_until(/[^\\]"/)
+          end
         elsif s.scan(/'/)
-          s.skip_until(/[^\\]'/)
+          if s.peek(1) == "'"
+            s.getch
+          else
+            s.skip_until(/[^\\]'/)
+          end
 
         # Skip number literals
-        elsif s.scan(/(0x)?\d+/)
+        elsif s.scan(/(0x)?\d(\d|\.)*/)
 
         # SGML style brackets
         elsif token = s.scan(/<[^\s<>][^<>]*>/)
           extract_sgml_tokens(token).each { |t| tokens << t }
 
         # Common programming punctuation
-        elsif token = s.scan(/;|\{|\}|\(|\)/)
+        elsif token = s.scan(/;|\{|\}|\(|\)|\[|\]/)
           tokens << token
 
         # Regular token
@@ -105,6 +113,33 @@ module Linguist
       tokens
     end
 
+    # Internal: Extract normalized shebang command token.
+    #
+    # Examples
+    #
+    #   extract_shebang("#!/usr/bin/ruby")
+    #   # => "ruby"
+    #
+    #   extract_shebang("#!/usr/bin/env node")
+    #   # => "node"
+    #
+    # Returns String token or nil it couldn't be parsed.
+    def extract_shebang(data)
+      s = StringScanner.new(data)
+
+      if path = s.scan(/^#!\s*\S+/)
+        script = path.split('/').last
+        if script == 'env'
+          s.scan(/\s+/)
+          script = s.scan(/\S+/)
+        end
+        script = script[/[^\d]+/, 0]
+        return script
+      end
+
+      nil
+    end
+
     # Internal: Extract tokens from inside SGML tag.
     #
     # data - SGML tag String.

samples/AppleScript/Convert To PDF.applescript

@@ -0,0 +1,87 @@
+(*
+Copyright 2003 Apple Computer, Inc.
+
+You may incorporate this Apple sample code into your program(s) without
+restriction.  This Apple sample code has been provided "AS IS" and the
+responsibility for its operation is yours.  You are not permitted to
+redistribute this Apple sample code as "Apple sample code" after having
+made changes.  If you're going to redistribute the code, we require
+that you make it clear that the code was descended from Apple sample
+code, but that you've made changes.
+*)
+
+property type_list : {"JPEG", "GIFf", "PICT", "TIFF", "PDF", "TEXT"}
+property extension_list : {"jpg", "gif", "pct", "tif", "pdf", "rtf"}
+--html is not currently handled
+
+on run {}
+	tell application "Finder" to set FinderSelection to the selection as alias list
+	
+	set FS to FinderSelection
+	--Ideally, this list could be passed to the open handler
+	
+	set SelectionCount to number of FS -- count	
+	if SelectionCount is 0 then
+		set FS to userPicksFolder()
+	else if the SelectionCount is 1 then
+		set MyPath to path to me
+		if MyPath is item 1 of FS then
+			--If I'm a droplet then I was double-clicked
+			set FS to userPicksFolder()
+		end if
+	else
+		--I'm not a double-clicked droplet
+	end if
+	open FS
+end run
+
+on userPicksFolder()
+	set these_items to {}
+	set these_items to (choose file with prompt "Select a file to convert to PDF:" of type {"JPEG", "GIFf", "PICT", "TIFF", "TEXT", "RTF"}) as list
+end userPicksFolder
+
+on open these_items
+	set thesefiles to {}
+	set the item_info to {}
+	repeat with i from 1 to the count of these_items
+		set this_item to (item i of these_items)
+		set the item_info to info for this_item
+		
+		if folder of the item_info is true then --if the item is a folder
+			processFolder(this_item)
+		else if ((folder of the item_info is false) and (alias of the item_info is false)) and (the file type of the item_info is in the type_list) or ((the name extension of the item_info) is in the extension_list) then
+			
+			set theFilePath to (item i of these_items as string)
+			set thePOSIXFilePath to POSIX path of theFilePath as string
+			processFile(thePOSIXFilePath)
+		end if
+	end repeat
+end open
+
+--process folders 
+on processFolder(theFolder)
+	set these_items to list folder theFolder without invisibles
+	repeat with i from 1 to the count of these_items
+		set this_item to alias ((theFolder as text) & (item i of these_items))
+		set the item_info to info for this_item
+		if folder of the item_info is true then
+			processFolder(this_item)
+		else if (alias of the item_info is false) and ((the file type of the item_info is in the type_list) or the name extension of the item_info is in the extension_list) then
+			set theFilePath to (this_item as string)
+			set thePOSIXFilePath to POSIX path of theFilePath as string
+			processFile(thePOSIXFilePath)
+		end if
+	end repeat
+end processFolder
+
+on processFile(thePOSIXFileName)
+	try
+		set terminalCommand to ""
+		set convertCommand to "/System/Library/Printers/Libraries/./convert "
+		set newFileName to thePOSIXFileName & ".pdf"
+		set terminalCommand to convertCommand & "-f " & "\"" & thePOSIXFileName & "\"" & " -o " & "\"" & newFileName & "\"" & " -j \"application/pdf\""
+		
+		do shell script terminalCommand
+	end try
+end processFile
+

samples/AppleScript/Convert To PostScript.applescript

@@ -0,0 +1,91 @@
+(*
+
+Copyright 2003 Apple Computer, Inc.
+
+You may incorporate this Apple sample code into your program(s) without
+restriction.  This Apple sample code has been provided "AS IS" and the
+responsibility for its operation is yours.  You are not permitted to
+redistribute this Apple sample code as "Apple sample code" after having
+made changes.  If you're going to redistribute the code, we require
+that you make it clear that the code was descended from Apple sample
+code, but that you've made changes.
+*)
+
+property type_list : {"JPEG", "GIFf", "PICT", "TIFF", "PDF", "TEXT"}
+property extension_list : {"jpg", "gif", "pct", "tif", "pdf", "rtf"}
+--html is not currently handled
+
+on run {}
+	tell application "Finder" to set FinderSelection to the selection as alias list
+	
+	set FS to FinderSelection
+	--Ideally, this list could be passed to the open handler
+	
+	set SelectionCount to number of FS -- count	
+	if SelectionCount is 0 then
+		set FS to userPicksFolder()
+	else if the SelectionCount is 1 then
+		set MyPath to path to me
+		if MyPath is item 1 of FS then
+			--If I'm a droplet then I was double-clicked
+			set FS to userPicksFolder()
+		end if
+	else
+		--I'm not a double-clicked droplet
+	end if
+	open FS
+end run
+
+on userPicksFolder()
+	set these_items to {}
+	set these_items to (choose file with prompt "Select a file to convert to PostScript:" of type {"JPEG", "GIFf", "PICT", "TIFF", "TEXT", "RTF"}) as list
+end userPicksFolder
+
+
+on open these_items
+	set thesefiles to {}
+	set the item_info to {}
+	repeat with i from 1 to the count of these_items
+		set this_item to (item i of these_items)
+		set the item_info to info for this_item
+		
+		if folder of the item_info is true then --if the item is a folder
+			processFolder(this_item)
+		else if ((folder of the item_info is false) and (alias of the item_info is false)) and (the file type of the item_info is in the type_list) or ((the name extension of the item_info) is in the extension_list) then
+			
+			set theFilePath to (item i of these_items as string)
+			set thePOSIXFilePath to POSIX path of theFilePath as string
+			processFile(thePOSIXFilePath)
+		end if
+	end repeat
+end open
+
+--process folders 
+on processFolder(theFolder)
+	set these_items to list folder theFolder without invisibles
+	repeat with i from 1 to the count of these_items
+		set this_item to alias ((theFolder as text) & (item i of these_items))
+		set the item_info to info for this_item
+		if folder of the item_info is true then
+			processFolder(this_item)
+		else if (alias of the item_info is false) and ((the file type of the item_info is in the type_list) or the name extension of the item_info is in the extension_list) then
+			set theFilePath to (this_item as string)
+			set thePOSIXFilePath to POSIX path of theFilePath as string
+			processFile(thePOSIXFilePath)
+		end if
+	end repeat
+end processFolder
+
+--need to pass the URL to Terminal
+on processFile(thePOSIXFileName)
+	try
+		set terminalCommand to ""
+		set convertCommand to "/System/Library/Printers/Libraries/./convert "
+		set newFileName to thePOSIXFileName & ".ps"
+		set terminalCommand to convertCommand & "-f " & "\"" & thePOSIXFileName & "\"" & " -o " & "\"" & newFileName & "\"" & " -j \"application/postscript\""
+		
+		do shell script terminalCommand
+	end try
+end processFile
+
+

samples/AppleScript/Count Messages in All Mailboxes.applescript

@@ -0,0 +1,80 @@
+(*
+Count Messages in All Mailboxes
+
+Copyright 2002-2012 Apple Inc. All rights reserved.
+
+You may incorporate this Apple sample code into your program(s) without
+restriction.  This Apple sample code has been provided "AS IS" and the
+responsibility for its operation is yours.  You are not permitted to
+redistribute this Apple sample code as "Apple sample code" after having
+made changes.  If you're going to redistribute the code, we require
+that you make it clear that the code was descended from Apple sample
+code, but that you've made changes.
+*)
+
+(*
+This script goes through each mailbox, gets the total message count and
+the unread count, then displays the final output in a new email message.
+*)
+
+tell application "Mail"
+	set localMailboxes to every mailbox
+	if (count of localMailboxes) is greater than 0 then
+		set messageCountDisplay to "Local mailboxes (On My Mac)" & return & my getMessageCountsForMailboxes(localMailboxes)
+	else
+		set messageCountDisplay to ""
+	end if
+	
+	set everyAccount to every account
+	repeat with eachAccount in everyAccount
+		set accountMailboxes to every mailbox of eachAccount
+		if (count of accountMailboxes) is greater than 0 then
+			set messageCountDisplay to messageCountDisplay & return & "Mailboxes for Account: " & name of eachAccount & return & my getMessageCountsForMailboxes(accountMailboxes)
+		end if
+	end repeat
+	
+	set outputMessage to make new outgoing message with properties {content:messageCountDisplay, subject:"Message counts for all my mailboxes", visible:true}
+	tell outputMessage
+		set font to "Courier"
+		set size to 12
+	end tell
+end tell
+
+on getMessageCountsForMailboxes(theMailboxes)
+	-- (list of mailboxes)
+	-- returns string
+	
+	set displayString to ""
+	
+	tell application "Mail"
+		repeat with eachMailbox in theMailboxes
+			set mailboxName to name of eachMailbox
+			set messageCount to (count of (messages of eachMailbox)) as string
+			set unreadCount to unread count of eachMailbox as string
+			
+			set displayString to displayString & "    " & my padString(mailboxName, 40) & "  " & messageCount & " (" & unreadCount & " unread)" & return
+		end repeat
+	end tell
+	
+	return displayString
+end getMessageCountsForMailboxes
+
+on padString(theString, fieldLength)
+	-- (string, integer)
+	-- returns string
+	
+	set stringLength to length of theString
+	
+	if stringLength is greater than fieldLength then
+		set paddedString to (text from character 1 to character (fieldLength - 3) of theString) & "..."
+	else -- stringLength is less than or equal to fieldLength
+		set paddedString to theString
+		
+		set paddingLength to fieldLength - stringLength
+		repeat paddingLength times
+			set paddedString to paddedString & space
+		end repeat
+	end if
+	
+	return paddedString
+end padString

samples/AppleScript/Crazy Message Text.applescript

@@ -0,0 +1,68 @@
+(*
+Crazy Message Text
+
+Copyright 2002-2012 Apple Inc. All rights reserved.
+
+You may incorporate this Apple sample code into your program(s) without
+restriction.  This Apple sample code has been provided "AS IS" and the
+responsibility for its operation is yours.  You are not permitted to
+redistribute this Apple sample code as "Apple sample code" after having
+made changes.  If you're going to redistribute the code, we require
+that you make it clear that the code was descended from Apple sample
+code, but that you've made changes.
+*)
+
+(*
+This script takes a string from the user and then makes a new message
+where each letter has a different font, size, and color.
+*)
+
+property lowFontSize : 36
+property highFontSize : 72
+property messageText : "Happy Birthday!"
+
+repeat
+	set userInput to display dialog "Enter some message text:" & return & return & "Minimum Character Size: " & (lowFontSize as string) & return & "Maximum Character Size: " & (highFontSize as string) default answer messageText buttons {"Cancel", "Set Prefs", "Continue"} default button 3
+	
+	if the button returned of userInput is "Set Prefs" then
+		set minimumFontSize to 9
+		
+		display dialog "Enter the minimum font size to use:" & return & return & "(Must be at least " & (minimumFontSize as string) & ")" default answer lowFontSize buttons {"OK"}
+		set newFontSize to text returned of the result as integer
+		if newFontSize is greater than or equal to minimumFontSize then
+			set lowFontSize to newFontSize
+		else
+			set lowFontSize to minimumFontSize
+		end if
+		
+		display dialog "Enter the maximum font size to use:" & return & return & "(Must be greater than " & (lowFontSize as string) & ")" default answer highFontSize buttons {"OK"}
+		set newFontSize to text returned of the result as integer
+		if newFontSize is greater than lowFontSize then
+			set highFontSize to newFontSize
+		else
+			set highFontSize to lowFontSize
+		end if
+		
+	else -- button returned of userInput is "Continue"
+		set theText to text returned of userInput
+		if theText is not "" then
+			set messageText to theText
+		end if
+		exit repeat
+	end if
+end repeat
+
+set fontList to {"American Typewriter", "American Typewriter Light", "American Typewriter Bold", "American Typewriter Condensed", "American Typewriter Condensed Light", "American Typewriter Condensed Bold", "Arial", "Arial Italic", "Arial Bold", "Arial Bold Italic", "Arial Black", "Baskerville", "Baskerville Italic", "Baskerville SemiBold", "Baskerville Bold", "Baskerville SemiBold Italic", "Baskerville Bold Italic", "Big Caslon Medium", "Comic Sans MS", "Comic Sans MS Bold", "Copperplate", "Copperplate Light", "Copperplate Bold", "Didot", "Didot Italic", "Didot Bold", "Futura Medium", "Futura Medium Italic", "Futura Condensed Medium", "Futura Condensed ExtraBold", "Geneva", "Gill Sans", "Gill Sans Italic", "Gill Sans Light", "Gill Sans Light Italic", "Gill Sans Bold", "Gill Sans Bold Italic", "Herculanum", "Lucida Grande", "Lucida Grande Bold", "Marker Felt Thin", "Marker Felt Wide", "Optima Regular", "Optima Italic", "Optima Bold", "Optima Bold Italic", "Optima ExtraBlack", "Papyrus", "Verdana", "Verdana Italic", "Verdana Bold", "Verdana Bold Italic", "Zapfino"}
+
+tell application "Mail"
+	activate
+	set crazyTextMessage to make new outgoing message with properties {content:messageText, visible:true}
+	
+	tell crazyTextMessage
+		repeat with eachCharacter in characters
+			set font of eachCharacter to (some item of fontList)
+			set size of eachCharacter to (random number from lowFontSize to highFontSize)
+			set color of eachCharacter to {random number from 0 to 65535, random number from 0 to 65535, random number from 0 to 65535}
+		end repeat
+	end tell
+end tell

samples/AppleScript/Get User Name.applescript

@@ -0,0 +1,41 @@
+(*
+Get User Name
+
+This script uses UI element scripting to get the name for the
+current user.
+
+If "Enable access for assistive devices" is not checked,
+this script will open the Universal Access System Preference and ask
+the user to check the checkbox.
+
+Copyright 2007 Apple Inc.
+
+You may incorporate this Apple sample code into your program(s) without
+restriction.  This Apple sample code has been provided "AS IS" and the
+responsibility for its operation is yours.  You are not permitted to
+redistribute this Apple sample code as "Apple sample code" after having
+made changes.  If you're going to redistribute the code, we require
+that you make it clear that the code was descended from Apple sample
+code, but that you've made changes.
+*)
+
+tell application "System Preferences"
+	activate
+	set current pane to pane "com.apple.preferences.users"
+end tell
+
+tell application "System Events"
+	if UI elements enabled then
+		tell tab group 1 of window "Accounts" of process "System Preferences"
+			click radio button 1
+			delay 2
+			get value of text field 1
+		end tell
+	else
+		tell application "System Preferences"
+			activate
+			set current pane to pane "com.apple.preference.universalaccess"
+			display dialog "UI element scripting is not enabled. Check \"Enable access for assistive devices\""
+		end tell
+	end if
+end tell

samples/AppleScript/Time Of Day.applescript

@@ -0,0 +1,75 @@
+(* 
+ Speaks the  date and time of day
+ 
+ Copyright 2008 Apple Inc. All rights reserved.
+ 
+ You may incorporate this Apple sample code into your program(s) without
+ restriction.  This Apple sample code has been provided "AS IS" and the
+ responsibility for its operation is yours.  You are not permitted to
+ redistribute this Apple sample code as "Apple sample code" after having
+ made changes.  If you're going to redistribute the code, we require
+ that you make it clear that the code was descended from Apple sample
+ code, but that you've made changes.
+ *)
+
+on isVoiceOverRunning()
+	set isRunning to false
+	tell application "System Events"
+		set isRunning to (name of processes) contains "VoiceOver"
+	end tell
+	return isRunning
+end isVoiceOverRunning
+
+on isVoiceOverRunningWithAppleScript()
+	if isVoiceOverRunning() then
+		set isRunningWithAppleScript to true
+		
+		-- is AppleScript enabled on VoiceOver --
+		tell application "VoiceOver"
+			try
+				set x to bounds of vo cursor
+			on error
+				set isRunningWithAppleScript to false
+			end try
+		end tell
+		return isRunningWithAppleScript
+	end if
+	return false
+end isVoiceOverRunningWithAppleScript
+
+set currentDate to current date
+set amPM to "AM"
+set currentHour to (currentDate's hours)
+set currentMinutes to currentDate's minutes
+
+if (currentHour > 12 and currentHour < 24) then
+	set amPM to "PM"
+else
+	set amPM to "AM"
+end if
+
+--  make minutes below 10 sound nice
+if currentMinutes < 10 then
+	set currentMinutes to ("0" & currentMinutes) as text
+end if
+
+--  ensure 0:nn gets set to 12:nn AM
+if currentHour is equal to 0 then
+	set currentHour to 12
+end if
+
+--  readjust for 12 hour time
+if (currentHour > 12) then
+	set currentHour to (currentHour - 12)
+end if
+
+set currentTime to ((currentDate's month) as text) & " " & ((currentDate's day) as text) & ", " & (currentHour as text) & ":" & ((currentMinutes) as text) & " " & amPM as text
+
+if isVoiceOverRunningWithAppleScript() then
+	tell application "VoiceOver"
+		output currentTime
+	end tell
+else
+	say currentTime
+	delay 2
+end if

samples/C++/qscicommand.h

@@ -0,0 +1,415 @@
+// This defines the interface to the QsciCommand class.
+//
+// Copyright (c) 2011 Riverbank Computing Limited <info@riverbankcomputing.com>
+// 
+// This file is part of QScintilla.
+// 
+// This file may be used under the terms of the GNU General Public
+// License versions 2.0 or 3.0 as published by the Free Software
+// Foundation and appearing in the files LICENSE.GPL2 and LICENSE.GPL3
+// included in the packaging of this file.  Alternatively you may (at
+// your option) use any later version of the GNU General Public
+// License if such license has been publicly approved by Riverbank
+// Computing Limited (or its successors, if any) and the KDE Free Qt
+// Foundation. In addition, as a special exception, Riverbank gives you
+// certain additional rights. These rights are described in the Riverbank
+// GPL Exception version 1.1, which can be found in the file
+// GPL_EXCEPTION.txt in this package.
+// 
+// If you are unsure which license is appropriate for your use, please
+// contact the sales department at sales@riverbankcomputing.com.
+// 
+// This file is provided AS IS with NO WARRANTY OF ANY KIND, INCLUDING THE
+// WARRANTY OF DESIGN, MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
+
+
+#ifndef QSCICOMMAND_H
+#define QSCICOMMAND_H
+
+#ifdef __APPLE__
+extern "C++" {
+#endif
+
+#include <qstring.h>
+
+#include <Qsci/qsciglobal.h>
+#include <Qsci/qsciscintillabase.h>
+
+
+class QsciScintilla;
+
+
+//! \brief The QsciCommand class represents an internal editor command that may
+//! have one or two keys bound to it.
+//!
+//! Methods are provided to change the keys bound to the command and to remove
+//! a key binding.  Each command has a user friendly description of the command
+//! for use in key mapping dialogs.
+class QSCINTILLA_EXPORT QsciCommand
+{
+public:
+    //! This enum defines the different commands that can be assigned to a key.
+    enum Command {
+        //! Move down one line.
+        LineDown = QsciScintillaBase::SCI_LINEDOWN,
+
+        //! Extend the selection down one line.
+        LineDownExtend = QsciScintillaBase::SCI_LINEDOWNEXTEND,
+
+        //! Extend the rectangular selection down one line.
+        LineDownRectExtend = QsciScintillaBase::SCI_LINEDOWNRECTEXTEND,
+
+        //! Scroll the view down one line.
+        LineScrollDown = QsciScintillaBase::SCI_LINESCROLLDOWN,
+
+        //! Move up one line.
+        LineUp = QsciScintillaBase::SCI_LINEUP,
+
+        //! Extend the selection up one line.
+        LineUpExtend = QsciScintillaBase::SCI_LINEUPEXTEND,
+
+        //! Extend the rectangular selection up one line.
+        LineUpRectExtend = QsciScintillaBase::SCI_LINEUPRECTEXTEND,
+
+        //! Scroll the view up one line.
+        LineScrollUp = QsciScintillaBase::SCI_LINESCROLLUP,
+
+        //! Scroll to the start of the document.
+        ScrollToStart = QsciScintillaBase::SCI_SCROLLTOSTART,
+
+        //! Scroll to the end of the document.
+        ScrollToEnd = QsciScintillaBase::SCI_SCROLLTOEND,
+
+        //! Scroll vertically to centre the current line.
+        VerticalCentreCaret = QsciScintillaBase::SCI_VERTICALCENTRECARET,
+
+        //! Move down one paragraph.
+        ParaDown = QsciScintillaBase::SCI_PARADOWN,
+
+        //! Extend the selection down one paragraph.
+        ParaDownExtend = QsciScintillaBase::SCI_PARADOWNEXTEND,
+
+        //! Move up one paragraph.
+        ParaUp = QsciScintillaBase::SCI_PARAUP,
+
+        //! Extend the selection up one paragraph.
+        ParaUpExtend = QsciScintillaBase::SCI_PARAUPEXTEND,
+
+        //! Move left one character.
+        CharLeft = QsciScintillaBase::SCI_CHARLEFT,
+
+        //! Extend the selection left one character.
+        CharLeftExtend = QsciScintillaBase::SCI_CHARLEFTEXTEND,
+
+        //! Extend the rectangular selection left one character.
+        CharLeftRectExtend = QsciScintillaBase::SCI_CHARLEFTRECTEXTEND,
+
+        //! Move right one character.
+        CharRight = QsciScintillaBase::SCI_CHARRIGHT,
+
+        //! Extend the selection right one character.
+        CharRightExtend = QsciScintillaBase::SCI_CHARRIGHTEXTEND,
+
+        //! Extend the rectangular selection right one character.
+        CharRightRectExtend = QsciScintillaBase::SCI_CHARRIGHTRECTEXTEND,
+
+        //! Move left one word.
+        WordLeft = QsciScintillaBase::SCI_WORDLEFT,
+
+        //! Extend the selection left one word.
+        WordLeftExtend = QsciScintillaBase::SCI_WORDLEFTEXTEND,
+
+        //! Move right one word.
+        WordRight = QsciScintillaBase::SCI_WORDRIGHT,
+
+        //! Extend the selection right one word.
+        WordRightExtend = QsciScintillaBase::SCI_WORDRIGHTEXTEND,
+
+        //! Move to the end of the previous word.
+        WordLeftEnd = QsciScintillaBase::SCI_WORDLEFTEND,
+
+        //! Extend the selection to the end of the previous word.
+        WordLeftEndExtend = QsciScintillaBase::SCI_WORDLEFTENDEXTEND,
+
+        //! Move to the end of the next word.
+        WordRightEnd = QsciScintillaBase::SCI_WORDRIGHTEND,
+
+        //! Extend the selection to the end of the next word.
+        WordRightEndExtend = QsciScintillaBase::SCI_WORDRIGHTENDEXTEND,
+
+        //! Move left one word part.
+        WordPartLeft = QsciScintillaBase::SCI_WORDPARTLEFT,
+
+        //! Extend the selection left one word part.
+        WordPartLeftExtend = QsciScintillaBase::SCI_WORDPARTLEFTEXTEND,
+
+        //! Move right one word part.
+        WordPartRight = QsciScintillaBase::SCI_WORDPARTRIGHT,
+
+        //! Extend the selection right one word part.
+        WordPartRightExtend = QsciScintillaBase::SCI_WORDPARTRIGHTEXTEND,
+
+        //! Move to the start of the document line.
+        Home = QsciScintillaBase::SCI_HOME,
+
+        //! Extend the selection to the start of the document line.
+        HomeExtend = QsciScintillaBase::SCI_HOMEEXTEND,
+
+        //! Extend the rectangular selection to the start of the document line.
+        HomeRectExtend = QsciScintillaBase::SCI_HOMERECTEXTEND,
+
+        //! Move to the start of the displayed line.
+        HomeDisplay = QsciScintillaBase::SCI_HOMEDISPLAY,
+
+        //! Extend the selection to the start of the displayed line.
+        HomeDisplayExtend = QsciScintillaBase::SCI_HOMEDISPLAYEXTEND,
+
+        //! Move to the start of the displayed or document line.
+        HomeWrap = QsciScintillaBase::SCI_HOMEWRAP,
+
+        //! Extend the selection to the start of the displayed or document
+        //! line.
+        HomeWrapExtend = QsciScintillaBase::SCI_HOMEWRAPEXTEND,
+
+        //! Move to the first visible character in the document line.
+        VCHome = QsciScintillaBase::SCI_VCHOME,
+
+        //! Extend the selection to the first visible character in the document
+        //! line.
+        VCHomeExtend = QsciScintillaBase::SCI_VCHOMEEXTEND,
+
+        //! Extend the rectangular selection to the first visible character in
+        //! the document line.
+        VCHomeRectExtend = QsciScintillaBase::SCI_VCHOMERECTEXTEND,
+
+        //! Move to the first visible character of the displayed or document
+        //! line.
+        VCHomeWrap = QsciScintillaBase::SCI_VCHOMEWRAP,
+
+        //! Extend the selection to the first visible character of the
+        //! displayed or document line.
+        VCHomeWrapExtend = QsciScintillaBase::SCI_VCHOMEWRAPEXTEND,
+
+        //! Move to the end of the document line.
+        LineEnd = QsciScintillaBase::SCI_LINEEND,
+
+        //! Extend the selection to the end of the document line.
+        LineEndExtend = QsciScintillaBase::SCI_LINEENDEXTEND,
+
+        //! Extend the rectangular selection to the end of the document line.
+        LineEndRectExtend = QsciScintillaBase::SCI_LINEENDRECTEXTEND,
+
+        //! Move to the end of the displayed line.
+        LineEndDisplay = QsciScintillaBase::SCI_LINEENDDISPLAY,
+
+        //! Extend the selection to the end of the displayed line.
+        LineEndDisplayExtend = QsciScintillaBase::SCI_LINEENDDISPLAYEXTEND,
+
+        //! Move to the end of the displayed or document line.
+        LineEndWrap = QsciScintillaBase::SCI_LINEENDWRAP,
+
+        //! Extend the selection to the end of the displayed or document line.
+        LineEndWrapExtend = QsciScintillaBase::SCI_LINEENDWRAPEXTEND,
+
+        //! Move to the start of the document.
+        DocumentStart = QsciScintillaBase::SCI_DOCUMENTSTART,
+
+        //! Extend the selection to the start of the document.
+        DocumentStartExtend = QsciScintillaBase::SCI_DOCUMENTSTARTEXTEND,
+
+        //! Move to the end of the document.
+        DocumentEnd = QsciScintillaBase::SCI_DOCUMENTEND,
+
+        //! Extend the selection to the end of the document.
+        DocumentEndExtend = QsciScintillaBase::SCI_DOCUMENTENDEXTEND,
+
+        //! Move up one page.
+        PageUp = QsciScintillaBase::SCI_PAGEUP,
+
+        //! Extend the selection up one page.
+        PageUpExtend = QsciScintillaBase::SCI_PAGEUPEXTEND,
+
+        //! Extend the rectangular selection up one page.
+        PageUpRectExtend = QsciScintillaBase::SCI_PAGEUPRECTEXTEND,
+
+        //! Move down one page.
+        PageDown = QsciScintillaBase::SCI_PAGEDOWN,
+
+        //! Extend the selection down one page.
+        PageDownExtend = QsciScintillaBase::SCI_PAGEDOWNEXTEND,
+
+        //! Extend the rectangular selection down one page.
+        PageDownRectExtend = QsciScintillaBase::SCI_PAGEDOWNRECTEXTEND,
+
+        //! Stuttered move up one page.
+        StutteredPageUp = QsciScintillaBase::SCI_STUTTEREDPAGEUP,
+
+        //! Stuttered extend the selection up one page.
+        StutteredPageUpExtend = QsciScintillaBase::SCI_STUTTEREDPAGEUPEXTEND,
+
+        //! Stuttered move down one page.
+        StutteredPageDown = QsciScintillaBase::SCI_STUTTEREDPAGEDOWN,
+
+        //! Stuttered extend the selection down one page.
+        StutteredPageDownExtend = QsciScintillaBase::SCI_STUTTEREDPAGEDOWNEXTEND,
+
+        //! Delete the current character.
+        Delete = QsciScintillaBase::SCI_CLEAR,
+
+        //! Delete the previous character.
+        DeleteBack = QsciScintillaBase::SCI_DELETEBACK,
+
+        //! Delete the previous character if not at start of line.
+        DeleteBackNotLine = QsciScintillaBase::SCI_DELETEBACKNOTLINE,
+
+        //! Delete the word to the left.
+        DeleteWordLeft = QsciScintillaBase::SCI_DELWORDLEFT,
+
+        //! Delete the word to the right.
+        DeleteWordRight = QsciScintillaBase::SCI_DELWORDRIGHT,
+
+        //! Delete right to the end of the next word.
+        DeleteWordRightEnd = QsciScintillaBase::SCI_DELWORDRIGHTEND,
+
+        //! Delete the line to the left.
+        DeleteLineLeft = QsciScintillaBase::SCI_DELLINELEFT,
+
+        //! Delete the line to the right.
+        DeleteLineRight = QsciScintillaBase::SCI_DELLINERIGHT,
+
+        //! Delete the current line.
+        LineDelete = QsciScintillaBase::SCI_LINEDELETE,
+
+        //! Cut the current line to the clipboard.
+        LineCut = QsciScintillaBase::SCI_LINECUT,
+
+        //! Copy the current line to the clipboard.
+        LineCopy = QsciScintillaBase::SCI_LINECOPY,
+
+        //! Transpose the current and previous lines.
+        LineTranspose = QsciScintillaBase::SCI_LINETRANSPOSE,
+
+        //! Duplicate the current line.
+        LineDuplicate = QsciScintillaBase::SCI_LINEDUPLICATE,
+
+        //! Select the whole document.
+        SelectAll = QsciScintillaBase::SCI_SELECTALL,
+
+        //! Move the selected lines up one line.
+        MoveSelectedLinesUp = QsciScintillaBase::SCI_MOVESELECTEDLINESUP,
+
+        //! Move the selected lines down one line.
+        MoveSelectedLinesDown = QsciScintillaBase::SCI_MOVESELECTEDLINESDOWN,
+
+        //! Duplicate the selection.
+        SelectionDuplicate = QsciScintillaBase::SCI_SELECTIONDUPLICATE,
+
+        //! Convert the selection to lower case.
+        SelectionLowerCase = QsciScintillaBase::SCI_LOWERCASE,
+
+        //! Convert the selection to upper case.
+        SelectionUpperCase = QsciScintillaBase::SCI_UPPERCASE,
+
+        //! Cut the selection to the clipboard.
+        SelectionCut = QsciScintillaBase::SCI_CUT,
+
+        //! Copy the selection to the clipboard.
+        SelectionCopy = QsciScintillaBase::SCI_COPY,
+
+        //! Paste from the clipboard.
+        Paste = QsciScintillaBase::SCI_PASTE,
+
+        //! Toggle insert/overtype.
+        EditToggleOvertype = QsciScintillaBase::SCI_EDITTOGGLEOVERTYPE,
+
+        //! Insert a platform dependent newline.
+        Newline = QsciScintillaBase::SCI_NEWLINE,
+
+        //! Insert a formfeed.
+        Formfeed = QsciScintillaBase::SCI_FORMFEED,
+
+        //! Indent one level.
+        Tab = QsciScintillaBase::SCI_TAB,
+
+        //! De-indent one level.
+        Backtab = QsciScintillaBase::SCI_BACKTAB,
+
+        //! Cancel any current operation.
+        Cancel = QsciScintillaBase::SCI_CANCEL,
+
+        //! Undo the last command.
+        Undo = QsciScintillaBase::SCI_UNDO,
+
+        //! Redo the last command.
+        Redo = QsciScintillaBase::SCI_REDO,
+
+        //! Zoom in.
+        ZoomIn = QsciScintillaBase::SCI_ZOOMIN,
+
+        //! Zoom out.
+        ZoomOut = QsciScintillaBase::SCI_ZOOMOUT,
+    };
+
+    //! Return the command that will be executed by this instance.
+    Command command() const {return scicmd;}
+
+    //! Execute the command.
+    void execute();
+
+    //! Binds the key \a key to the command.  If \a key is 0 then the key
+    //! binding is removed.  If \a key is invalid then the key binding is
+    //! unchanged.  Valid keys are any visible or control character or any
+    //! of \c Key_Down, \c Key_Up, \c Key_Left, \c Key_Right, \c Key_Home,
+    //! \c Key_End, \c Key_PageUp, \c Key_PageDown, \c Key_Delete,
+    //! \c Key_Insert, \c Key_Escape, \c Key_Backspace, \c Key_Tab and
+    //! \c Key_Return.  Keys may be modified with any combination of \c SHIFT,
+    //! \c CTRL, \c ALT and \c META.
+    //!
+    //! \sa key(), setAlternateKey(), validKey()
+    void setKey(int key);
+
+    //! Binds the alternate key \a altkey to the command.  If \a key is 0
+    //! then the alternate key binding is removed.
+    //!
+    //! \sa alternateKey(), setKey(), validKey()
+    void setAlternateKey(int altkey);
+
+    //! The key that is currently bound to the command is returned.
+    //!
+    //! \sa setKey(), alternateKey()
+    int key() const {return qkey;}
+
+    //! The alternate key that is currently bound to the command is
+    //! returned.
+    //!
+    //! \sa setAlternateKey(), key()
+    int alternateKey() const {return qaltkey;}
+
+    //! If the key \a key is valid then true is returned.
+    static bool validKey(int key);
+
+    //! The user friendly description of the command is returned.
+    QString description() const;
+
+private:
+    friend class QsciCommandSet;
+
+    QsciCommand(QsciScintilla *qs, Command cmd, int key, int altkey,
+            const char *desc);
+
+    void bindKey(int key,int &qk,int &scik);
+
+    QsciScintilla *qsCmd;
+    Command scicmd;
+    int qkey, scikey, qaltkey, scialtkey;
+    const char *descCmd;
+
+    QsciCommand(const QsciCommand &);
+    QsciCommand &operator=(const QsciCommand &);
+};
+
+#ifdef __APPLE__
+}
+#endif
+
+#endif

samples/C++/qsciprinter.h

@@ -0,0 +1,116 @@
+// This module defines interface to the QsciPrinter class.
+//
+// Copyright (c) 2011 Riverbank Computing Limited <info@riverbankcomputing.com>
+// 
+// This file is part of QScintilla.
+// 
+// This file may be used under the terms of the GNU General Public
+// License versions 2.0 or 3.0 as published by the Free Software
+// Foundation and appearing in the files LICENSE.GPL2 and LICENSE.GPL3
+// included in the packaging of this file.  Alternatively you may (at
+// your option) use any later version of the GNU General Public
+// License if such license has been publicly approved by Riverbank
+// Computing Limited (or its successors, if any) and the KDE Free Qt
+// Foundation. In addition, as a special exception, Riverbank gives you
+// certain additional rights. These rights are described in the Riverbank
+// GPL Exception version 1.1, which can be found in the file
+// GPL_EXCEPTION.txt in this package.
+// 
+// If you are unsure which license is appropriate for your use, please
+// contact the sales department at sales@riverbankcomputing.com.
+// 
+// This file is provided AS IS with NO WARRANTY OF ANY KIND, INCLUDING THE
+// WARRANTY OF DESIGN, MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
+
+
+#ifndef QSCIPRINTER_H
+#define QSCIPRINTER_H
+
+#ifdef __APPLE__
+extern "C++" {
+#endif
+
+#include <qprinter.h>
+
+#include <Qsci/qsciglobal.h>
+#include <Qsci/qsciscintilla.h>
+
+
+QT_BEGIN_NAMESPACE
+class QRect;
+class QPainter;
+QT_END_NAMESPACE
+
+class QsciScintillaBase;
+
+
+//! \brief The QsciPrinter class is a sub-class of the Qt QPrinter class that
+//! is able to print the text of a Scintilla document.
+//!
+//! The class can be further sub-classed to alter to layout of the text, adding
+//! headers and footers for example.
+class QSCINTILLA_EXPORT QsciPrinter : public QPrinter
+{
+public:
+    //! Constructs a printer paint device with mode \a mode.
+    QsciPrinter(PrinterMode mode = ScreenResolution);
+
+    //! Destroys the QsciPrinter instance.
+    virtual ~QsciPrinter();
+
+    //! Format a page, by adding headers and footers for example, before the
+    //! document text is drawn on it.  \a painter is the painter to be used to
+    //! add customised text and graphics.  \a drawing is true if the page is
+    //! actually being drawn rather than being sized.  \a painter drawing
+    //! methods must only be called when \a drawing is true.  \a area is the
+    //! area of the page that will be used to draw the text.  This should be
+    //! modified if it is necessary to reserve space for any customised text or
+    //! graphics.  By default the area is relative to the printable area of the
+    //! page.  Use QPrinter::setFullPage() because calling printRange() if you
+    //! want to try and print over the whole page.  \a pagenr is the number of
+    //! the page.  The first page is numbered 1.
+    virtual void formatPage(QPainter &painter, bool drawing, QRect &area,
+            int pagenr);
+
+    //! Return the number of points to add to each font when printing.
+    //!
+    //! \sa setMagnification()
+    int magnification() const {return mag;}
+
+    //! Sets the number of points to add to each font when printing to \a
+    //! magnification.
+    //!
+    //! \sa magnification()
+    virtual void setMagnification(int magnification);
+
+    //! Print a range of lines from the Scintilla instance \a qsb.  \a from is
+    //! the first line to print and a negative value signifies the first line
+    //! of text.  \a to is the last line to print and a negative value
+    //! signifies the last line of text.  true is returned if there was no
+    //! error.
+    virtual int printRange(QsciScintillaBase *qsb, int from = -1, int to = -1);
+
+    //! Return the line wrap mode used when printing.  The default is
+    //! QsciScintilla::WrapWord.
+    //!
+    //! \sa setWrapMode()
+    QsciScintilla::WrapMode wrapMode() const {return wrap;}
+
+    //! Sets the line wrap mode used when printing to \a wmode.
+    //!
+    //! \sa wrapMode()
+    virtual void setWrapMode(QsciScintilla::WrapMode wmode);
+
+private:
+    int mag;
+    QsciScintilla::WrapMode wrap;
+
+    QsciPrinter(const QsciPrinter &);
+    QsciPrinter &operator=(const QsciPrinter &);
+};
+
+#ifdef __APPLE__
+}
+#endif
+
+#endif

samples/Ceylon/Foo.ceylon

@@ -0,0 +1,15 @@
+doc "Test function for Ceylon"
+by  "Enrique"
+shared void test() {
+  print("test");
+}
+
+doc "Test class for Ceylon"
+shared class Test(name) satisfies Comparable<Test> {
+    shared String name;
+    shared actual String string = "Test " name ".";
+
+    shared actual Comparison compare(Test other) {
+        return name<=>other.name;
+    }
+}

samples/Coq/Basics.v

@@ -0,0 +1,707 @@
+Inductive day : Type :=
+| monday : day
+| tuesday : day
+| wednesday : day
+| thursday : day
+| friday : day
+| saturday : day
+| sunday : day.
+
+Definition next_weekday (d:day) : day :=
+  match d with
+  | monday => tuesday
+  | tuesday => wednesday
+  | wednesday => thursday
+  | thursday => friday
+  | friday => monday
+  | saturday => monday
+  | sunday => monday
+  end.
+
+Example test_next_weekday:
+(next_weekday (next_weekday saturday)) = tuesday.
+
+Proof. simpl. reflexivity. Qed.
+
+Inductive bool : Type :=
+	| true : bool
+	| false : bool.
+
+Definition negb (b:bool) : bool :=
+													 match b with
+																			 | true => false
+																			 | false => true
+													 end.
+
+Definition andb (b1:bool) (b2:bool) : bool :=
+		match b1 with
+		 | true => b2
+		 | false => false
+	  end.
+
+Definition orb (b1:bool) (b2:bool) : bool :=
+		match b1 with
+		  | true => true
+		  | false => b2
+		end.
+
+Example test_orb1: (orb true false) = true.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb2: (orb false false) = false.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb3: (orb false true) = true.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb4: (orb true true) = true.
+Proof. simpl. reflexivity. Qed.
+
+Definition nandb (b1: bool) (b2:bool) : bool :=
+	match b1 with
+		| true => match b2 with
+										| false => true
+										| true => false
+							end
+		| false => true
+	end.
+
+Example test_nandb1: (nandb true false) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb2: (nandb false false) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb3: (nandb false true) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb4: (nandb true true) = false.
+Proof. simpl. reflexivity. Qed.
+
+Definition andb3 (b1: bool) (b2:bool) (b3:bool) : bool :=
+	match b1 with
+    | false => false
+		| true => match b2 with
+								| false => false
+								| true => b3
+							end
+	end.
+
+Example test_andb31: (andb3 true true true) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_andb32: (andb3 false true true) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_andb33: (andb3 true false true) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_andb34: (andb3 true true false) = false.
+Proof. simpl. reflexivity. Qed.
+
+Module Playground1.
+
+Inductive nat : Type :=
+	| O : nat
+	| S : nat -> nat.
+
+Definition pred (n : nat) : nat :=
+	match n with
+		| O => O
+		| S n' => n'
+	end.
+
+Definition minustwo (n : nat) : nat :=
+	match n with
+		| O => O
+		| S O => O
+		| S (S n') => n'
+	end.
+
+Fixpoint evenb (n : nat) : bool :=
+	match n with
+		| O => true
+		| S O => false
+		| S (S n') => evenb n'
+	end.
+
+Definition oddb (n : nat) : bool := negb (evenb n).
+
+Example test_oddb1: (oddb (S O)) = true.
+Proof. reflexivity. Qed.
+Example test_oddb2: (oddb (S (S (S (S O))))) = false.
+Proof. reflexivity. Qed.
+
+Fixpoint plus (n : nat) (m : nat) : nat :=
+	match n with
+		| O => m
+		| S n' => S (plus n' m)
+	end.
+
+Fixpoint mult (n m : nat) : nat :=
+	match n with
+		| O => O
+		| S n' => plus m (mult n' m)
+	end.
+
+Fixpoint minus (n m : nat) : nat :=
+	match n, m with
+		| O, _ => n
+		| S n', O => S n'
+		| S n', S m' => minus n' m'
+	end.
+
+Fixpoint exp (base power : nat) : nat :=
+	match power with
+		| O => S O
+		| S p => mult base (exp base p)
+	end.
+
+Fixpoint factorial (n : nat) : nat :=
+	match n with
+		| O => S O
+		| S n' => mult n (factorial n')
+	end.
+
+Example test_factorial1: (factorial (S (S (S O)))) = (S (S (S (S (S (S O)))))).
+Proof. simpl. reflexivity. Qed.
+
+Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
+Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope.
+Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope.
+
+Fixpoint beq_nat (n m : nat) : bool :=
+	match n with
+		| O => match m with
+						| O => true
+						| S m' => false
+					 end
+		| S n' => match m with
+							| O => false
+							| S m' => beq_nat n' m'
+							end
+	end.
+
+Fixpoint ble_nat (n m : nat) : bool :=
+	match n with
+		| O => true
+		| S n' => 
+				match m with
+					| O => false
+					| S m' => ble_nat n' m'
+				end
+	end.
+
+Example test_ble_nat1: (ble_nat (S (S O)) (S (S O))) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_ble_nat2: (ble_nat (S (S O)) (S (S (S (S O))))) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_ble_nat3: (ble_nat (S (S (S (S O)))) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+
+Definition blt_nat (n m : nat) : bool :=
+		(andb (negb (beq_nat n m)) (ble_nat n m)).
+
+Example test_blt_nat1: (blt_nat (S (S O)) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_blt_nat3: (blt_nat (S (S (S (S O)))) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_blt_nat2 : (blt_nat (S (S O)) (S (S (S (S O))))) = true.
+Proof. simpl. reflexivity. Qed.
+
+Theorem plus_O_n : forall n : nat, O + n = n.
+Proof.
+	simpl. reflexivity. Qed.
+
+Theorem plus_O_n' : forall n : nat, O + n = n.
+Proof.
+	reflexivity. Qed.
+
+Theorem plus_O_n'' : forall n : nat, O + n = n.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem plus_1_1 : forall n : nat, (S O) + n = S n.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem mult_0_1: forall n : nat, O * n = O.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem plus_id_example : forall n m:nat,
+	n = m -> n + n = m + m.
+Proof.
+	intros n m.
+	intros H.
+	rewrite -> H.
+	reflexivity. Qed.
+
+Theorem plus_id_exercise : forall n m o: nat,
+	n = m -> m = o -> n + m = m + o.
+Proof.
+	intros n m o.
+	intros H.
+	intros H'.
+	rewrite -> H.
+	rewrite <- H'.
+	reflexivity.
+	Qed.
+
+Theorem mult_0_plus : forall n m : nat,
+				(O + n) * m = n * m.
+Proof.
+	intros n m.
+	rewrite -> plus_O_n.
+	reflexivity. Qed.
+
+Theorem mult_1_plus : forall n m: nat,
+	((S O) + n) * m = m + (n * m).
+Proof.
+	intros n m.
+	rewrite -> plus_1_1.
+	reflexivity.
+	Qed.
+
+Theorem mult_1 : forall n : nat,
+				n * (S O) = n.
+Proof.
+	intros n.
+	induction n as [| n'].
+	reflexivity.
+	simpl.
+	rewrite -> IHn'.
+	reflexivity.
+	Qed.
+
+Theorem plus_1_neq_0 : forall n : nat,
+				beq_nat (n + (S O)) O = false.
+Proof.
+	intros n.
+	destruct n as [| n'].
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem zero_nbeq_plus_1 : forall n : nat,
+				beq_nat O (n + (S O)) = false.
+Proof.
+	intros n.
+	destruct n.
+	reflexivity.
+	reflexivity.
+Qed.
+
+Require String. Open Scope string_scope.
+
+Ltac move_to_top x :=
+match reverse goal with
+| H : _ |- _ => try move x after H
+end.
+
+Tactic Notation "assert_eq" ident(x) constr(v) :=
+	let H := fresh in
+	assert (x = v) as H by reflexivity;
+	clear H.
+
+	Tactic Notation "Case_aux" ident(x) constr(name) :=
+		first [
+		set (x := name); move_to_top x
+		| assert_eq x name; move_to_top x
+		| fail 1 "because we are working on a different case" ].
+
+		Ltac Case name := Case_aux Case name.
+		Ltac SCase name := Case_aux SCase name.
+		Ltac SSCase name := Case_aux SSCase name.
+		Ltac SSSCase name := Case_aux SSSCase name.
+		Ltac SSSSCase name := Case_aux SSSSCase name.
+		Ltac SSSSSCase name := Case_aux SSSSSCase name.
+		Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
+		Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.
+
+Theorem andb_true_elim1 : forall b c : bool,
+				andb b c = true -> b = true.
+Proof.
+	intros b c H.
+	destruct b.
+	Case "b = true".
+		reflexivity.
+	Case "b = false".
+		rewrite <- H. reflexivity. Qed.
+
+Theorem plus_0_r : forall n : nat, n + O = n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0". reflexivity.
+	Case "n = S n'". simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem minus_diag : forall n,
+				minus n n = O.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		simpl. reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+
+Theorem mult_0_r : forall n:nat,
+				n * O = O.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem plus_n_Sm : forall n m : nat,
+				S (n + m) = n + (S m).
+Proof.
+	intros n m. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem plus_assoc : forall n m p : nat,
+					n + (m + p) = (n + m) + p.
+Proof.
+	intros n m p.
+	induction n as [| n'].
+	reflexivity.
+	simpl.
+	rewrite -> IHn'.
+	reflexivity. Qed.
+
+Theorem plus_distr : forall n m: nat, S (n + m) = n + (S m).
+Proof.
+	intros n m.  induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem mult_distr : forall n m: nat, n * ((S O) + m) = n * (S m).
+Proof.
+	intros n m.
+	induction n as [| n'].
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem plus_comm : forall n m : nat,
+	n + m = m + n.
+Proof.
+	intros n m.
+	induction n as [| n'].
+	Case "n = 0".
+		simpl.
+		rewrite -> plus_0_r.
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		rewrite -> IHn'.
+		rewrite -> plus_distr.
+		reflexivity. Qed.
+
+Fixpoint double (n:nat) :=
+	match n with
+		| O => O
+		| S n' => S (S (double n'))
+	end.
+
+Lemma double_plus : forall n, double n = n + n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'.
+		rewrite -> plus_distr. reflexivity.
+		Qed.
+
+Theorem beq_nat_refl : forall n : nat,
+	true = beq_nat n n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n".
+		simpl. rewrite <- IHn'.
+		reflexivity. Qed.
+
+Theorem plus_rearrange: forall n m p q : nat,
+				(n + m) + (p + q) = (m + n) + (p + q).
+Proof.
+	intros n m p q.
+	assert(H: n + m = m + n).
+		Case "Proof by assertion".
+		rewrite -> plus_comm. reflexivity.
+	rewrite -> H. reflexivity. Qed.
+
+Theorem plus_swap : forall n m p: nat,
+				n + (m + p) = m + (n + p).
+Proof.
+	intros n m p.
+	rewrite -> plus_assoc.
+	assert(H: m + (n + p) = (m + n) + p).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H.
+	assert(H2: m + n = n + m).
+	rewrite -> plus_comm.
+	reflexivity.
+	rewrite -> H2.
+	reflexivity.
+	Qed.
+
+Theorem plus_swap' : forall n m p: nat,
+				n + (m + p) = m + (n + p).
+Proof.
+	intros n m p.
+	rewrite -> plus_assoc.
+	assert(H: m + (n + p) = (m + n) + p).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H.
+	replace (m + n) with (n + m).
+	rewrite -> plus_comm.
+	reflexivity.
+	rewrite -> plus_comm.
+	reflexivity.
+	Qed.
+
+Theorem mult_1_distr: forall m n: nat,
+				n * ((S O) + m) = n * (S O) + n * m.
+Proof.
+	intros n m.
+	rewrite -> mult_1.
+	rewrite -> plus_1_1.
+	simpl.
+	induction m as [|m'].
+	simpl.
+	reflexivity.
+	simpl.
+	rewrite -> plus_swap.
+	rewrite <- IHm'.
+	reflexivity.
+	Qed.
+
+Theorem mult_comm: forall m n : nat,
+				m * n = n * m.
+Proof.
+	intros m n.
+	induction n as [| n'].
+	Case "n = 0".
+		simpl.
+		rewrite -> mult_0_r.
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		rewrite <- mult_distr.
+		rewrite -> mult_1_distr.
+		rewrite -> mult_1.
+		rewrite -> IHn'.
+		reflexivity.
+		Qed.
+
+Theorem evenb_next : forall n : nat,
+				evenb n = evenb (S (S n)).
+Proof.
+	intros n.
+Admitted.
+
+Theorem negb_negb : forall n : bool,
+				n = negb (negb n).
+Proof.
+	intros n.
+	destruct n.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem evenb_n_oddb_Sn : forall n : nat,
+				evenb n = negb (evenb (S n)).
+Proof.
+	intros n.
+	induction n as [|n'].
+	reflexivity.
+	assert(H: evenb n' = evenb (S (S n'))).
+	reflexivity.
+	rewrite <- H.
+	rewrite -> IHn'.
+	rewrite <- negb_negb.
+	reflexivity.
+	Qed.
+
+(*Fixpoint bad (n : nat) : bool :=
+	match n with
+		| O => true
+		| S O => bad (S n)
+		| S (S n') => bad n'
+	end.*)
+
+Theorem ble_nat_refl : forall n:nat,
+				true = ble_nat n n.
+Proof.
+	intros n.
+	induction n as [|n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n".
+		simpl.
+		rewrite <- IHn'.
+		reflexivity.
+	Qed.
+
+Theorem zero_nbeq_S : forall n: nat,
+				beq_nat O (S n) = false.
+Proof.
+	intros n.
+	reflexivity.
+	Qed.
+
+Theorem andb_false_r : forall b : bool,
+				andb b false = false.
+Proof.
+	intros b.
+	destruct b.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem plus_ble_compat_1 : forall n m p : nat,
+				ble_nat n m = true -> ble_nat (p + n) (p + m) = true.
+Proof.
+	intros n m p.
+	intros H.
+	induction p.
+	Case "p = 0".
+		simpl.
+		rewrite -> H.
+		reflexivity.
+	Case "p = S p'".
+		simpl.
+		rewrite -> IHp.
+		reflexivity.
+		Qed.
+
+Theorem S_nbeq_0 : forall n:nat,
+				beq_nat (S n) O = false.
+Proof.
+	intros n.
+	reflexivity.
+	Qed.
+
+Theorem mult_1_1 : forall n:nat, (S O) * n = n.
+Proof.
+	intros n.
+	simpl.
+	rewrite -> plus_0_r.
+	reflexivity. Qed.
+
+Theorem all3_spec : forall b c : bool,
+	orb (andb b c)
+			(orb (negb b)
+			 		 (negb c))
+	= true.
+Proof.
+	intros b c.
+	destruct b.
+	destruct c.
+	reflexivity.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Lemma mult_plus_1 : forall n m : nat,
+			S(m + n) = m + (S n).
+Proof.
+	intros n m.
+	induction m.
+	reflexivity.
+	simpl.
+	rewrite -> IHm.
+	reflexivity.
+	Qed.
+
+Theorem mult_mult : forall n m : nat,
+	n * (S m) = n * m + n.
+Proof.
+	intros n m.
+	induction n.
+	reflexivity.
+	simpl.
+	rewrite -> IHn.
+	rewrite -> plus_assoc.
+	rewrite -> mult_plus_1.
+	reflexivity.
+	Qed.
+
+Theorem mult_plus_distr_r : forall n m p:nat,
+				(n + m) * p = (n * p) + (m * p).
+Proof.
+	intros n m p.
+	induction p.
+	rewrite -> mult_0_r.
+	rewrite -> mult_0_r.
+	rewrite -> mult_0_r.
+	reflexivity.
+	rewrite -> mult_mult.
+	rewrite -> mult_mult.
+	rewrite -> mult_mult.
+	rewrite -> IHp.
+	assert(H1: ((n * p) + n) + (m * p + m) = (n * p) + (n + (m * p + m))).
+	rewrite <- plus_assoc.
+	reflexivity.
+	rewrite -> H1.
+	assert(H2: (n + (m * p + m)) = (m * p + (n + m))).
+	rewrite -> plus_swap.
+	reflexivity.
+	rewrite -> H2.
+	assert(H3: (n * p) + (m * p + (n + m)) = ((n * p ) + (m * p)) + (n + m)).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H3.
+	reflexivity.
+	Qed.
+
+Theorem mult_assoc : forall n m p : nat,
+				n * (m * p) = (n * m) * p.
+Proof.
+	intros n m p.
+	induction n.
+	simpl.
+	reflexivity.
+	simpl.
+	rewrite -> mult_plus_distr_r.
+	rewrite -> IHn.
+	reflexivity.
+	Qed.
+
+Inductive bin : Type :=
+	| BO : bin
+	| D : bin -> bin
+	| M : bin -> bin.
+
+Fixpoint incbin (n : bin) : bin :=
+	match n with
+		| BO => M (BO)
+		| D n' => M n'
+		| M n' => D (incbin n')
+	end.
+
+Fixpoint bin2un (n : bin) : nat :=
+	match n with
+		| BO => O
+		| D n' => double (bin2un n')
+		| M n' => S (double (bin2un n'))
+	end.
+
+Theorem bin_comm : forall n : bin,
+				bin2un(incbin n) = S (bin2un n).
+Proof.
+	intros n.
+	induction n.
+		reflexivity.
+		reflexivity.
+		simpl.
+		rewrite -> IHn.
+		reflexivity.
+	Qed.
+
+End Playground1.

samples/Coq/Heap.v

@@ -0,0 +1,300 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
+
+(** A development of Treesort on Heap trees. It has an average
+    complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
+    the list is already sorted) *)
+
+(* G. Huet 1-9-95 uses Multiset *)
+
+Require Import List Multiset PermutSetoid Relations Sorting.
+
+Section defs.
+
+  (** * Trees and heap trees *)
+
+  (** ** Definition of trees over an ordered set *)
+
+  Variable A : Type.
+  Variable leA : relation A.
+  Variable eqA : relation A.
+
+  Let gtA (x y:A) := ~ leA x y.
+
+  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
+
+  Hint Resolve leA_refl.
+  Hint Immediate eqA_dec leA_dec leA_antisym.
+
+  Let emptyBag := EmptyBag A.
+  Let singletonBag := SingletonBag _ eqA_dec.
+
+  Inductive Tree :=
+    | Tree_Leaf : Tree
+    | Tree_Node : A -> Tree -> Tree -> Tree.
+
+  (** [a] is lower than a Tree [T] if [T] is a Leaf
+      or [T] is a Node holding [b>a] *)
+
+  Definition leA_Tree (a:A) (t:Tree) :=
+    match t with
+      | Tree_Leaf => True
+      | Tree_Node b T1 T2 => leA a b
+    end.
+
+  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
+  Proof.
+    simpl; auto with datatypes.
+  Qed.
+
+  Lemma leA_Tree_Node :
+    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
+  Proof.
+    simpl; auto with datatypes.
+  Qed.
+
+
+  (** ** The heap property *)
+
+  Inductive is_heap : Tree -> Prop :=
+    | nil_is_heap : is_heap Tree_Leaf
+    | node_is_heap :
+      forall (a:A) (T1 T2:Tree),
+        leA_Tree a T1 ->
+        leA_Tree a T2 ->
+        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
+
+  Lemma invert_heap :
+    forall (a:A) (T1 T2:Tree),
+      is_heap (Tree_Node a T1 T2) ->
+      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
+  Proof.
+    intros; inversion H; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rect :
+    forall P:Tree -> Type,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN.
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply X0; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rec :
+    forall P:Tree -> Set,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN.
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply X; auto with datatypes.
+  Qed.
+
+  Lemma low_trans :
+    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros; simpl; apply leA_trans with b; auto with datatypes.
+  Qed.
+
+  (** ** Merging two sorted lists *)
+
+  Inductive merge_lem (l1 l2:list A) : Type :=
+    merge_exist :
+    forall l:list A,
+      Sorted leA l ->
+      meq (list_contents _ eqA_dec l)
+      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
+      (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
+      merge_lem l1 l2.
+  Require Import Morphisms.
+  
+  Instance: Equivalence (@meq A).
+  Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
+
+  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
+  Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
+  
+  Lemma merge :
+    forall l1:list A, Sorted leA l1 ->
+    forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
+  Proof.
+    fix 1; intros; destruct l1.
+    apply merge_exist with l2; auto with datatypes.
+    rename l1 into l.
+    revert l2 H0. fix 1. intros.
+    destruct l2 as [|a0 l0]. 
+    apply merge_exist with (a :: l); simpl; auto with datatypes. 
+    elim (leA_dec a a0); intros.
+
+    (* 1 (leA a a0) *)
+    apply Sorted_inv in H. destruct H.
+    destruct (merge l H (a0 :: l0) H0).
+    apply merge_exist with (a :: l1). clear merge merge0.
+      auto using cons_sort, cons_leA with datatypes.
+    simpl. rewrite m. now rewrite munion_ass. 
+    intros. apply cons_leA. 
+    apply (@HdRel_inv _ leA) with l; trivial with datatypes.
+
+    (* 2 (leA a0 a) *)
+    apply Sorted_inv in H0. destruct H0.
+    destruct (merge0 l0 H0). clear merge merge0.  
+    apply merge_exist with (a0 :: l1); 
+      auto using cons_sort, cons_leA with datatypes.
+    simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
+    repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
+    intros. apply cons_leA. 
+    apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
+  Qed.
+
+  (** ** From trees to multisets *)
+
+  (** contents of a tree as a multiset *)
+
+  (** Nota Bene : In what follows the definition of SingletonBag
+      in not used. Actually, we could just take as postulate:
+      [Parameter SingletonBag : A->multiset].  *)
+
+  Fixpoint contents (t:Tree) : multiset A :=
+    match t with
+      | Tree_Leaf => emptyBag
+      | Tree_Node a t1 t2 =>
+	munion (contents t1) (munion (contents t2) (singletonBag a))
+    end.
+
+
+  (** equivalence of two trees is equality of corresponding multisets *)
+  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
+
+
+
+  (** * From lists to sorted lists *)
+
+  (** ** Specification of heap insertion *)
+
+  Inductive insert_spec (a:A) (T:Tree) : Type :=
+    insert_exist :
+    forall T1:Tree,
+      is_heap T1 ->
+      meq (contents T1) (munion (contents T) (singletonBag a)) ->
+      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
+      insert_spec a T.
+
+
+  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
+  Proof.
+    simple induction 1; intros.
+    apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl; unfold meq, munion; auto using node_is_heap with datatypes.
+    elim (leA_dec a a0); intros.
+    elim (X a0); intros.
+    apply insert_exist with (Tree_Node a T2 T0);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl; apply treesort_twist1; trivial with datatypes.
+    elim (X a); intros T3 HeapT3 ConT3 LeA.
+    apply insert_exist with (Tree_Node a0 T2 T3);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply low_trans with a; auto with datatypes.
+    apply LeA; auto with datatypes.
+    apply low_trans with a; auto with datatypes.
+    simpl; apply treesort_twist2; trivial with datatypes.
+  Qed.
+
+
+  (** ** Building a heap from a list *)
+
+  Inductive build_heap (l:list A) : Type :=
+    heap_exist :
+    forall T:Tree,
+      is_heap T ->
+      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
+
+  Lemma list_to_heap : forall l:list A, build_heap l.
+  Proof.
+    simple induction l.
+    apply (heap_exist nil Tree_Leaf); auto with datatypes.
+    simpl; unfold meq; exact nil_is_heap.
+    simple induction 1.
+    intros T i m; elim (insert T i a).
+    intros; apply heap_exist with T1; simpl; auto with datatypes.
+    apply meq_trans with (munion (contents T) (singletonBag a)).
+    apply meq_trans with (munion (singletonBag a) (contents T)).
+    apply meq_right; trivial with datatypes.
+    apply munion_comm.
+    apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** ** Building the sorted list *)
+
+  Inductive flat_spec (T:Tree) : Type :=
+    flat_exist :
+    forall l:list A,
+      Sorted leA l ->
+      (forall a:A, leA_Tree a T -> HdRel leA a l) ->
+      meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
+
+  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
+  Proof.
+    intros T h; elim h; intros.
+    apply flat_exist with (nil (A:=A)); auto with datatypes.
+    elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
+    elim (merge _ s1 _ s2); intros.
+    apply flat_exist with (a :: l); simpl; auto with datatypes.
+    apply meq_trans with
+      (munion (list_contents _ eqA_dec l1)
+	(munion (list_contents _ eqA_dec l2) (singletonBag a))).
+    apply meq_congr; auto with datatypes.
+    apply meq_trans with
+      (munion (singletonBag a)
+	(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
+    apply munion_rotate.
+    apply meq_right; apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** * Specification of treesort *)
+
+  Theorem treesort :
+    forall l:list A,
+    {m : list A | Sorted leA m & permutation _ eqA_dec l m}.
+  Proof.
+    intro l; unfold permutation.
+    elim (list_to_heap l).
+    intros.
+    elim (heap_to_list T); auto with datatypes.
+    intros.
+    exists l0; auto with datatypes.
+    apply meq_trans with (contents T); trivial with datatypes.
+  Qed.
+
+End defs.

samples/Coq/Lists.v

@@ -0,0 +1,591 @@
+Require Export Basics.
+Module NatList.
+Import Playground1.
+
+Inductive natprod : Type :=
+	pair : nat -> nat -> natprod.
+
+Definition fst (p : natprod) : nat :=
+	match p with
+		| pair x y => x
+	end.
+
+Definition snd (p : natprod) : nat :=
+	match p with
+		| pair x y => y
+	end.
+
+Notation "( x , y )" := (pair x y).
+
+Definition swap_pair (p : natprod) : natprod :=
+	match p with
+			| (x, y) => (y, x)
+	end.
+
+Theorem surjective_pairing' : forall (n m : nat),
+	(n, m) = (fst (n, m), snd (n, m)).
+Proof.
+	reflexivity.  Qed.
+
+Theorem surjective_pairing : forall (p : natprod),
+	p = (fst p, snd p).
+Proof.
+	intros p.
+	destruct p as (n, m).
+	simpl.
+	reflexivity.
+	Qed.
+
+Theorem snd_fst_is_swap : forall (p : natprod),
+	(snd p, fst p) = swap_pair p.
+Proof.
+	intros p.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Theorem fst_swap_is_snd : forall (p : natprod),
+	 fst (swap_pair p) = snd p.
+Proof.
+	intros p.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Inductive natlist : Type :=
+	| nil : natlist
+	| cons : nat -> natlist -> natlist.
+
+Definition l_123 := cons (S O) (cons (S (S O)) (cons (S (S (S O))) nil)).
+
+Notation "x :: l" := (cons x l) (at level 60, right associativity).
+Notation "[ ]" := nil.
+Notation "[]" := nil.
+Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
+
+Fixpoint repeat (n count : nat) : natlist :=
+	match count with
+		| O => nil
+		| S count' => n :: (repeat n count')
+	end.
+
+Fixpoint length (l:natlist) : nat :=
+	match l with
+		| nil => O
+		| h :: t => S (length t)
+	end.
+
+Fixpoint app (l1 l2 : natlist) : natlist :=
+	match l1 with
+		| nil => l2
+		| h :: t => h :: (app t l2)
+	end.
+
+Notation "x ++ y" := (app x y) (right associativity, at level 60).
+
+(*
+Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
+Proof. reflexivity. Qed.
+Example test_app2: nil ++ [4,5] = [4,5].
+Proof. reflexivity. Qed.
+Example test_app3: [1,2,3] ++ [] = [1,2,3].
+Proof. reflexivity. Qed.
+*)
+
+Definition head (l : natlist) : nat :=
+	match l with
+		| nil => O
+		| h :: t => h
+	end.
+
+Definition tl (l : natlist) : natlist :=
+	match l with
+		| nil => nil
+		| h :: t => t
+	end.
+
+			(*
+Example test_tl: tl [1,2,3] = [2,3].
+Proof. reflexivity. Qed.
+*)
+
+Fixpoint nonzeros (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| O :: r => nonzeros r
+		| n :: r => n :: (nonzeros r)
+	end.
+
+Example test_nonzeros: nonzeros [O,S O,O,S (S O), S (S (S O)),O,O] = [S O,S (S O), S (S (S O))].
+Proof. reflexivity. Qed.
+
+Fixpoint oddmembers (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| n :: r => match (oddb n) with
+										| true => n :: (oddmembers r)
+										| false => oddmembers r
+								end
+	end.
+
+Example test_oddmembers: oddmembers [O, S O, O, S (S O), S (S (S O)), O, O] = [S O, S (S (S O))].
+Proof. reflexivity. Qed.
+
+Fixpoint countoddmembers (l:natlist) : nat :=
+		length (oddmembers l).
+
+Example test_countoddmembers2: countoddmembers [O, S (S O), S (S (S (S O)))] = O.
+Proof. reflexivity. Qed.
+
+Example test_countoddmembers3: countoddmembers [] = O.
+Proof. reflexivity. Qed.
+
+Fixpoint alternate (l1 l2 : natlist) : natlist :=
+		match l1 with
+				| nil => l2
+				| a :: r1 => match l2 with
+											| nil => l1
+											| b :: r2 => a :: b :: (alternate r1 r2)
+										end
+		end.
+
+Example test_alternative1: alternate [S O, S (S O), S (S (S O))] [S (S (S (S O))), S (S (S (S (S O)))), S (S (S (S (S (S O)))))] =
+		[S O, S (S (S (S O))), S (S O), S (S (S (S (S O)))), S (S (S O)), S (S (S (S (S (S O)))))].
+Proof. reflexivity. Qed.
+
+Definition bag := natlist.
+
+Fixpoint count (v : nat) (s: bag) : nat :=
+	match s with
+		| nil => O
+		| v' :: r => match (beq_nat v' v) with
+										| true => S (count v r)
+										| false => count v r
+								 end
+	end.
+
+Example test_count1: count (S O) [S O, S (S O), S (S (S O)), S O, S (S (S (S O))), S O] = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition sum : bag -> bag -> bag := app.
+
+Example test_sum1: count (S O) (sum [S O, S (S O), S (S (S O))] [S O, S (S (S (S O))), S O]) = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition add (v:nat) (s:bag) : bag := v :: s.
+
+Example test_add1: count (S O) (add (S O) [S O, S (S (S (S O))), S O]) = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition member (v:nat) (s:bag) : bool :=
+	ble_nat (S O) (count v s).
+
+Example test_member1: member (S O) [S O, S (S (S (S O))), S O] = true.
+Proof. reflexivity. Qed.
+
+Example test_member2: member (S (S O)) [S O, S (S (S (S O))), S O] = false.
+Proof. reflexivity. Qed.
+
+Fixpoint remove_one (v:nat) (s:bag) : bag :=
+	match s with
+		| nil => nil
+		| v' :: r => match (beq_nat v v') with
+									| true => r
+									| false => v' :: (remove_one v r)
+								 end
+	end.
+
+Example test_remove_one1: count (S (S (S (S (S O)))))
+																(remove_one (S (S (S (S (S O)))))
+																[S (S O), S O, S (S (S (S (S O)))), S (S (S (S O))), S O]) = O.
+Proof. reflexivity. Qed.
+
+Fixpoint remove_all (v:nat) (s:bag) : bag :=
+	match s with
+		| nil => nil
+		| v' :: r => match (beq_nat v v') with
+										| true => remove_all v r
+										| false => v' :: (remove_all v r)
+								 end
+	end.
+
+Example test_remove_all1: count (S (S (S (S (S O)))))
+																(remove_all (S (S (S (S (S O)))))
+																[S (S O), S O, S (S (S (S (S O)))), S (S (S (S O))), S O]) = O.
+Proof. reflexivity. Qed.
+
+Fixpoint subset (s1:bag) (s2:bag) : bool :=
+		match s1 with
+			| nil => true
+			| v :: r => andb (member v s2)
+											 (subset r (remove_one v s2))
+		end.
+
+Definition test_subset1: subset [S O, S (S O)] [S (S O), S O, S (S (S (S O))), S O] = true.
+Proof. reflexivity. Qed.
+Definition test_subset2: subset [S O, S (S O), S (S O)] [S (S O), S O, S (S (S (S O))), S O] = false.
+Proof. reflexivity. Qed.
+
+Theorem bag_count_add : forall n t: nat, forall s : bag,
+				count n s = t -> count n (add n s) = S t.
+Proof.
+	intros n t s.
+	intros H.
+	induction s.
+	simpl.
+	rewrite <- beq_nat_refl.
+	rewrite <- H.
+	reflexivity.
+	rewrite <- H.
+	simpl.
+	rewrite <- beq_nat_refl.
+	reflexivity.
+Qed.
+
+Theorem nil_app : forall l:natlist,
+	[] ++ l = l.
+Proof.
+	reflexivity. Qed.
+
+Theorem tl_length_pred : forall l:natlist,
+	pred (length l) = length (tl l).
+Proof.
+	intros l. destruct l as [| n l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons n l'".
+		reflexivity. Qed.
+
+Theorem app_ass:forall l1 l2 l3 : natlist,
+	(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+Proof.
+	intros l1 l2 l3. induction l1 as [| n l1'].
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons n l1'".
+		simpl. rewrite -> IHl1'. reflexivity. Qed.
+
+Theorem app_length: forall l1 l2 : natlist,
+	length (l1 ++ l2) = (length l1) + (length l2).
+Proof.
+	intros l1 l2. induction l1 as [| n l1'].
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons".
+		simpl. rewrite -> IHl1'. reflexivity. Qed.
+
+Fixpoint snoc (l:natlist) (v:nat) : natlist :=
+	match l with
+		| nil => [v]
+		| h :: t => h :: (snoc t v)
+	end.
+
+Fixpoint rev (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| h :: t => snoc (rev t) h
+	end.
+
+Example test_rev1: rev [S O, S (S O), S (S (S O))] = [S (S (S O)), S (S O), S O].
+Proof. reflexivity. Qed.
+
+Theorem length_snoc : forall n : nat, forall l : natlist,
+	length (snoc l n) = S (length l).
+Proof.
+	intros n l. induction l as [| n' l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons n' l'".
+		simpl. rewrite -> IHl'. reflexivity. Qed.
+
+Theorem rev_length : forall l : natlist,
+	length (rev l) = length l.
+Proof.
+	intros l. induction l as [| n l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl. rewrite -> length_snoc.
+		rewrite -> IHl'. reflexivity. Qed.
+
+Theorem app_nil_end : forall l :natlist,
+	l ++ [] = l.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl. rewrite -> IHl. reflexivity. Qed.
+
+
+
+Theorem rev_snoc : forall l: natlist, forall n : nat,
+	rev (snoc l n) = n :: (rev l).
+Proof.
+	intros l n.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem rev_involutive : forall l : natlist,
+	rev (rev l) = l.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> rev_snoc.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem app_ass4 : forall l1 l2 l3 l4 : natlist,
+	l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
+Proof.
+	intros l1 l2 l3 l4.
+	rewrite -> app_ass.
+	rewrite -> app_ass.
+	reflexivity.
+	Qed.
+
+Theorem snoc_append : forall (l : natlist) (n : nat),
+	snoc l n = l ++ [n].
+Proof.
+	intros l n.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem nonzeros_length : forall l1 l2 : natlist,
+	nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
+Proof.
+	intros l1 l2.
+	induction l1.
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons".
+		simpl.
+		rewrite -> IHl1.
+		destruct n.
+		reflexivity.
+		reflexivity.
+		Qed.
+
+Theorem distr_rev : forall l1 l2 : natlist,
+	rev (l1 ++ l2) = (rev l2) ++ (rev l1).
+Proof.
+	intros l1 l2.
+	induction l1.
+	Case "l1 = nil".
+		simpl.
+		rewrite -> app_nil_end.
+		reflexivity.
+	Case "l1 = cons".
+		simpl.
+		rewrite -> IHl1.
+		simpl.
+		rewrite -> snoc_append.
+		rewrite -> snoc_append.
+		rewrite -> app_ass.
+		reflexivity.
+		Qed.
+
+Theorem count_number_nonzero : forall (s : bag),
+	ble_nat O (count (S O) (S O :: s)) = true.
+Proof.
+	intros s.
+	induction s.
+		reflexivity.
+		reflexivity.
+		Qed.
+
+Theorem ble_n_Sn : forall n,
+	ble_nat n (S n) = true.
+Proof.
+	intros n. induction n as [| n'].
+	Case "0".
+		simpl. reflexivity.
+	Case "S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem remove_decreases_count: forall (s : bag),
+	ble_nat (count O (remove_one O s)) (count O s) = true.
+Proof.
+	intros s.
+	induction s.
+	Case "s = nil".
+		reflexivity.
+	Case "s = cons".
+		simpl.
+		induction n.
+		SCase "n = O".
+			simpl.  rewrite -> ble_n_Sn.
+			reflexivity.
+		SCase "n = S n'".
+			simpl.
+			rewrite -> IHs.
+			reflexivity.
+			Qed.
+
+Inductive natoption : Type :=
+	| Some : nat -> natoption
+	| None : natoption.
+
+Fixpoint index (n:nat) (l:natlist) : natoption :=
+	match l with
+		| nil => None
+		| a :: l' => if beq_nat n O then Some a else index (pred n) l'
+  end.
+
+Definition option_elim (o : natoption) (d : nat) : nat :=
+	match o with
+		| Some n' => n'
+		| None => d
+	end.
+
+Definition hd_opt (l : natlist) : natoption :=
+	match l with
+		| nil => None
+		| v :: r => Some v
+	end.
+
+Example test_hd_opt1 : hd_opt [] = None.
+Proof. reflexivity. Qed.
+Example test_hd_opt2 : hd_opt [S O] = Some (S O).
+Proof. reflexivity. Qed.
+
+Theorem option_elim_hd : forall l:natlist,
+	head l = option_elim (hd_opt l) O.
+Proof.
+	intros l.
+	destruct l.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
+	match l1 with
+		| nil => match l2 with
+							| nil => true
+							| _ => false
+						 end
+		| v1 :: r1 => match l2 with
+									 | nil => false
+									 | v2 :: r2 => if beq_nat v1 v2 then beq_natlist r1 r2
+																 else false
+									end
+	end.
+
+Example test_beq_natlist1 : (beq_natlist nil nil = true).
+Proof. reflexivity. Qed.
+Example test_beq_natlist2 : (beq_natlist [S O, S (S O), S (S (S O))]
+																				 [S O, S (S O), S (S (S O))] = true).
+Proof. reflexivity. Qed.
+
+Theorem beq_natlist_refl : forall l:natlist,
+	beq_natlist l l = true.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite <- beq_nat_refl.
+		rewrite -> IHl.
+		reflexivity.
+	Qed.
+
+Theorem silly1 : forall (n m o p : nat),
+	n = m -> [n, o] = [n, p] -> [n, o] = [m, p].
+Proof.
+	intros n m o p eq1 eq2.
+	rewrite <- eq1.
+	apply eq2. Qed.
+
+Theorem silly2a : forall (n m : nat),
+	(n,n) = (m,m) ->
+		(forall (q r : nat), (q, q) = (r, r) -> [q] = [r]) ->
+			[n] = [m].
+Proof.
+	intros n m eq1 eq2.
+	apply eq2.
+	apply eq1.
+	Qed.
+
+Theorem silly_ex :
+	(forall n, evenb n = true -> oddb (S n) = true) ->
+	evenb (S (S (S O))) = true ->
+	oddb (S (S (S (S O)))) = true.
+Proof.
+	intros eq1 eq2.
+	apply eq1.
+	apply eq2.
+	Qed.
+
+Theorem silly3 : forall (n : nat),
+	true = beq_nat n (S (S (S (S (S O))))) ->
+	beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))) = true.
+Proof.
+	intros n H.
+	symmetry.
+	apply H.
+	Qed.
+
+Theorem rev_exercise : forall (l l' : natlist),
+	l = rev l' -> l' = rev l.
+Proof.
+	intros l l' H.
+	rewrite -> H.
+	rewrite -> rev_involutive.
+	reflexivity.
+	Qed.
+
+Theorem beq_nat_sym : forall (n m:nat), forall (b: bool),
+	beq_nat n m = b -> beq_nat m n = b.
+Proof.
+	intros n.
+	induction n as [| n'].
+	Case "n = O".
+		intros m b eq1.
+		induction m.
+		SCase "m = 0".
+			apply eq1.
+		SCase "m = S m'".
+			apply eq1.
+	Case "n = S n'".
+		induction m.
+		SCase "m = 0".
+			intros b eq1.
+			apply eq1.
+		SCase "m = S m'".
+			intros b eq1.
+			apply IHn'.
+			apply eq1.
+		Qed.
+
+Theorem app_ass' : forall l1 l2 l3 : natlist,
+	(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+Proof.
+	intros l1. induction l1 as [ | n l1'].
+	reflexivity.
+	simpl.
+	intros l2 l3.
+	rewrite -> IHl1'.
+	reflexivity.
+	Qed.
+
+End NatList.

samples/Coq/PermutSetoid.v

@@ -0,0 +1,547 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Omega Relations Multiset SetoidList.
+
+(** This file is deprecated, use [Permutation.v] instead.
+
+    Indeed, this file defines a notion of permutation based on
+    multisets (there exists a permutation between two lists iff every
+    elements have the same multiplicity in the two lists) which
+    requires a more complex apparatus (the equipment of the domain
+    with a decidable equality) than [Permutation] in [Permutation.v].
+
+    The relation between the two relations are in lemma
+    [permutation_Permutation].
+
+    File [Permutation] concerns Leibniz equality : it shows in particular
+    that [List.Permutation] and [permutation] are equivalent in this context.
+*)
+
+Set Implicit Arguments.
+
+Local Notation "[ ]" := nil.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
+
+Section Permut.
+
+(** * From lists to multisets *)
+
+Variable A : Type.
+Variable eqA : relation A.
+Hypothesis eqA_equiv : Equivalence eqA.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
+
+(** contents of a list *)
+
+Fixpoint list_contents (l:list A) : multiset A :=
+  match l with
+  | [] => emptyBag
+  | a :: l => munion (singletonBag a) (list_contents l)
+  end.
+
+Lemma list_contents_app :
+  forall l m:list A,
+    meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
+Proof.
+  simple induction l; simpl; auto with datatypes.
+  intros.
+  apply meq_trans with
+    (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
+    auto with datatypes.
+Qed.
+
+(** * [permutation]: definition and basic properties *)
+
+Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
+
+Lemma permut_refl : forall l:list A, permutation l l.
+Proof.
+  unfold permutation; auto with datatypes.
+Qed.
+
+Lemma permut_sym :
+  forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
+Proof.
+  unfold permutation, meq; intros; symmetry; trivial.
+Qed.
+
+Lemma permut_trans :
+  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
+Proof.
+  unfold permutation; intros.
+  apply meq_trans with (list_contents m); auto with datatypes.
+Qed.
+
+Lemma permut_cons_eq :
+  forall l m:list A,
+    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
+Proof.
+  unfold permutation; simpl; intros.
+  apply meq_trans with (munion (singletonBag a') (list_contents l)).
+  apply meq_left, meq_singleton; auto.
+  auto with datatypes.
+Qed.
+
+Lemma permut_cons :
+  forall l m:list A,
+    permutation l m -> forall a:A, permutation (a :: l) (a :: m).
+Proof.
+  unfold permutation; simpl; auto with datatypes.
+Qed.
+
+Lemma permut_app :
+  forall l l' m m':list A,
+    permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
+Proof.
+  unfold permutation; intros.
+  apply meq_trans with (munion (list_contents l) (list_contents m));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m'));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m));
+    auto using permut_cons, list_contents_app with datatypes.
+Qed.
+
+Lemma permut_add_inside_eq :
+  forall a a' l1 l2 l3 l4, eqA a a' ->
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  specialize H0 with a0.
+  repeat rewrite list_contents_app in *; simpl in *.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+    decide (eqA_dec a' a0) with Ha; simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_inside :
+  forall a l1 l2 l3 l4,
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  generalize (H a0); clear H.
+  do 4 rewrite list_contents_app.
+  simpl.
+  destruct (eqA_dec a a0); simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_cons_inside_eq :
+  forall a a' l l1 l2, eqA a a' ->
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a' :: l2).
+Proof.
+  intros;
+  replace (a :: l) with ([] ++ a :: l); trivial;
+    apply permut_add_inside_eq; trivial.
+Qed.
+
+Lemma permut_add_cons_inside :
+  forall a l l1 l2,
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a :: l2).
+Proof.
+  intros;
+    replace (a :: l) with ([] ++ a :: l); trivial;
+	apply permut_add_inside; trivial.
+Qed.
+
+Lemma permut_middle :
+  forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
+Proof.
+  intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
+Qed.
+
+Lemma permut_sym_app :
+  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
+Proof.
+  intros l1 l2;
+    unfold permutation, meq;
+	intro a; do 2 rewrite list_contents_app; simpl;
+	  auto with arith.
+Qed.
+
+Lemma permut_rev :
+  forall l, permutation l (rev l).
+Proof.
+  induction l.
+  simpl; trivial using permut_refl.
+  simpl.
+  apply permut_add_cons_inside.
+  rewrite <- app_nil_end. trivial.
+Qed.
+
+(** * Some inversion results. *)
+Lemma permut_conv_inv :
+  forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
+Proof.
+  intros e l1 l2; unfold permutation, meq; simpl; intros H a;
+    generalize (H a); apply plus_reg_l.
+Qed.
+
+Lemma permut_app_inv1 :
+  forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  rewrite plus_comm; rewrite H; rewrite plus_comm.
+  trivial.
+Qed.
+
+(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
+
+Fact if_eqA_then : forall a a' (B:Type)(b b':B),
+ eqA a a' -> (if eqA_dec a a' then b else b') = b.
+Proof.
+  intros. destruct eqA_dec as [_|NEQ]; auto.
+  contradict NEQ; auto.
+Qed.
+
+Lemma permut_app_inv2 :
+  forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  trivial.
+Qed.
+
+Lemma permut_remove_hd_eq :
+  forall l l1 l2 a b, eqA a b ->
+    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
+  specialize H with a0.
+  rewrite list_contents_app in *; simpl in *.
+  apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
+  rewrite H; clear H.
+  symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.
+  rewrite plus_comm.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
+    decide (eqA_dec b a0) with Ha; reflexivity.
+Qed.
+
+Lemma permut_remove_hd :
+  forall l l1 l2 a,
+    permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  eauto using permut_remove_hd_eq, Equivalence_Reflexive.
+Qed.
+
+Fact if_eqA_else : forall a a' (B:Type)(b b':B),
+ ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
+Proof.
+  intros. decide (eqA_dec a a') with H; auto.
+Qed.
+
+Fact if_eqA_refl : forall a (B:Type)(b b':B),
+ (if eqA_dec a a then b else b') = b.
+Proof.
+  intros; apply (decide_left (eqA_dec a a)); auto with *.
+Qed.
+
+(** PL: Inutilisable dans un rewrite sans un change prealable. *)
+
+Global Instance if_eqA (B:Type)(b b':B) :
+ Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
+Proof.
+ intros x x' Hxx' y y' Hyy'.
+ intros; destruct (eqA_dec x y) as [H|H];
+  destruct (eqA_dec x' y') as [H'|H']; auto.
+ contradict H'; transitivity x; auto with *; transitivity y; auto with *.
+ contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
+Qed.
+
+Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
+ eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1' a2 then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A1|A1];
+  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
+ contradict A1'; transitivity a1; eauto with *.
+ contradict A1; transitivity a1'; eauto with *.
+Qed.
+
+Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
+ eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1 a2' then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A2|A2];
+  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
+ contradict A2'; transitivity a2; eauto with *.
+ contradict A2; transitivity a2'; eauto with *.
+Qed.
+
+
+Global Instance multiplicity_eqA (l:list A) :
+ Proper (eqA==>@eq _) (multiplicity (list_contents l)).
+Proof.
+  intros x x' Hxx'.
+  induction l as [|y l Hl]; simpl; auto.
+  rewrite (@if_eqA_rewrite_r y x x'); auto.
+Qed.
+
+Lemma multiplicity_InA :
+  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
+Proof.
+  induction l.
+  simpl.
+  split; inversion 1.
+  simpl.
+  intros a'; split; intros H. inversion_clear H.
+  apply (decide_left (eqA_dec a a')); auto with *.
+  destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
+  destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
+Qed.
+
+Lemma multiplicity_InA_O :
+  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
+Proof.
+  intros l a; rewrite multiplicity_InA;
+    destruct (multiplicity (list_contents l) a); auto with arith.
+  destruct 1; auto with arith.
+Qed.
+
+Lemma multiplicity_InA_S :
+  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
+Proof.
+  intros l a; rewrite multiplicity_InA; auto with arith.
+Qed.
+
+Lemma multiplicity_NoDupA : forall l,
+  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
+Proof.
+  induction l.
+  simpl.
+  split; auto with arith.
+  split; simpl.
+  inversion_clear 1.
+  rewrite IHl in H1.
+  intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
+  rewrite <- EQ.
+  rewrite multiplicity_InA_O; auto.
+  intros; constructor.
+  rewrite multiplicity_InA.
+  specialize (H a).
+  rewrite if_eqA_refl in H.
+  clear IHl; omega.
+  rewrite IHl; intros.
+  specialize (H a0). omega.
+Qed.
+
+(** Permutation is compatible with InA. *)
+Lemma permut_InA_InA :
+  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
+Proof.
+  intros l1 l2 e.
+  do 2 rewrite multiplicity_InA.
+  unfold permutation, meq.
+  intros H;rewrite H; auto.
+Qed.
+
+Lemma permut_cons_InA :
+  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
+Proof.
+  intros; apply (permut_InA_InA (e:=e) H); auto with *.
+Qed.
+
+(** Permutation of an empty list. *)
+Lemma permut_nil :
+  forall l, permutation l [] -> l = [].
+Proof.
+  intro l; destruct l as [ | e l ]; trivial.
+  assert (InA eqA e (e::l)) by (auto with *).
+  intro Abs; generalize (permut_InA_InA Abs H).
+  inversion 1.
+Qed.
+
+(** Permutation for short lists. *)
+
+Lemma permut_length_1:
+  forall a b, permutation [a] [b] -> eqA a b.
+Proof.
+  intros a b; unfold permutation, meq.
+  intro P; specialize (P b); simpl in *.
+  rewrite if_eqA_refl in *.
+  destruct (eqA_dec a b); simpl; auto; discriminate.
+Qed.
+
+Lemma permut_length_2 :
+  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
+    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
+Proof.
+  intros a1 b1 a2 b2 P.
+  assert (H:=permut_cons_InA P).
+  inversion_clear H.
+  left; split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  specialize (P a). simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega.
+  right.
+  inversion_clear H0; [|inversion H].
+  split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  specialize (P a); simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega.
+Qed.
+
+(** Permutation is compatible with length. *)
+Lemma permut_length :
+  forall l1 l2, permutation l1 l2 -> length l1 = length l2.
+Proof.
+  induction l1; intros l2 H.
+  rewrite (permut_nil (permut_sym H)); auto.
+  assert (H0:=permut_cons_InA H).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite app_length.
+  simpl; rewrite <- plus_n_Sm; f_equal.
+  rewrite <- app_length.
+  apply IHl1.
+  apply permut_remove_hd with b.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  rewrite (@if_eqA_rewrite_l a b a0); auto.
+Qed.
+
+Lemma NoDupA_equivlistA_permut :
+  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
+    equivlistA eqA l l' -> permutation l l'.
+Proof.
+  intros.
+  red; unfold meq; intros.
+  rewrite multiplicity_NoDupA in H, H0.
+  generalize (H a) (H0 a) (H1 a); clear H H0 H1.
+  do 2 rewrite multiplicity_InA.
+  destruct 3; omega.
+Qed.
+
+End Permut.
+
+Section Permut_map.
+
+Variables A B : Type.
+
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Variable eqB : B->B->Prop.
+Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
+Hypothesis eqB_trans : Transitive eqB.
+
+(** Permutation is compatible with map. *)
+
+Lemma permut_map :
+  forall f,
+    (Proper (eqA==>eqB) f) ->
+    forall l1 l2, permutation _ eqA_dec l1 l2 ->
+      permutation _ eqB_dec (map f l1) (map f l2).
+Proof.
+  intros f; induction l1.
+  intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.
+  intros l2 P.
+  simpl.
+  assert (H0:=permut_cons_InA eqA_equiv P).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite map_app.
+  simpl.
+  apply permut_trans with (f b :: map f l1).
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  destruct (eqB_dec (f b) a0) as [H2|H2];
+    destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
+  destruct H3; transitivity (f b); auto with *.
+  destruct H2; transitivity (f a); auto with *.
+  apply permut_add_cons_inside.
+  rewrite <- map_app.
+  apply IHl1; auto.
+  apply permut_remove_hd with b; trivial.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
+Qed.
+
+End Permut_map.
+
+Require Import Permutation.
+
+Section Permut_permut.
+
+Variable A : Type.
+
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Lemma Permutation_impl_permutation : forall l l',
+  Permutation l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons; auto using Equivalence_Reflexive.
+    change (x :: y :: l) with ([x] ++ y :: l);
+      apply permut_add_cons_inside; simpl;
+      apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl.
+    apply permut_trans with l'; trivial.
+Qed.
+
+Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons_eq; trivial.
+Qed.
+
+Lemma permutation_Permutation : forall l l',
+  permutation _ eqA_dec l l' <->
+  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
+Proof.
+  split; intro H.
+  (* -> *)
+  induction l in l', H |- *.
+    exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.
+    pose proof H as H'.
+    apply permut_cons_InA, InA_split in H
+      as (l1 & y & l2 & Heq & ->); trivial.
+    apply permut_remove_hd_eq, IHl in H'
+      as (l'' & IHP & IHA); clear IHl; trivial.
+    apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).
+    exists (l1'' ++ a :: l2''); split.
+      apply Permutation_cons_app; trivial.
+      apply Forall2_app, Forall2_cons; trivial.
+  (* <- *)
+  destruct H as (l'' & H & Heq).
+  apply permut_trans with l''.
+    apply Permutation_impl_permutation; trivial.
+    apply permut_eqA; trivial.
+Qed.
+
+End Permut_permut.
+
+(* begin hide *)
+(** For compatibilty *)
+Notation permut_right := permut_cons (only parsing).
+Notation permut_tran := permut_trans (only parsing).
+(* end hide *)

samples/Coq/Permutation.v

@@ -0,0 +1,644 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*********************************************************************)
+(** * List permutations as a composition of adjacent transpositions  *)
+(*********************************************************************)
+
+(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
+   Laurent Théry (Huffmann contribution, October 2003) *)
+
+Require Import List Setoid Compare_dec Morphisms.
+Import ListNotations. (* For notations [] and [a;b;c] *)
+Set Implicit Arguments.
+
+Section Permutation.
+
+Variable A:Type.
+
+Inductive Permutation : list A -> list A -> Prop :=
+| perm_nil: Permutation [] []
+| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
+| perm_swap x y l : Permutation (y::x::l) (x::y::l)
+| perm_trans l l' l'' :
+    Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+
+Local Hint Constructors Permutation.
+
+(** Some facts about [Permutation] *)
+
+Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
+Proof.
+  intros l HF.
+  remember (@nil A) as m in HF.
+  induction HF; discriminate || auto.
+Qed.
+
+Theorem Permutation_nil_cons : forall (l : list A) (x : A),
+ ~ Permutation nil (x::l).
+Proof.
+  intros l x HF.
+  apply Permutation_nil in HF; discriminate.
+Qed.
+
+(** Permutation over lists is a equivalence relation *)
+
+Theorem Permutation_refl : forall l : list A, Permutation l l.
+Proof.
+  induction l; constructor. exact IHl.
+Qed.
+
+Theorem Permutation_sym : forall l l' : list A,
+ Permutation l l' -> Permutation l' l.
+Proof.
+  intros l l' Hperm; induction Hperm; auto.
+  apply perm_trans with (l':=l'); assumption.
+Qed.
+
+Theorem Permutation_trans : forall l l' l'' : list A,
+ Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+Proof.
+  exact perm_trans.
+Qed.
+
+End Permutation.
+
+Hint Resolve Permutation_refl perm_nil perm_skip.
+
+(* These hints do not reduce the size of the problem to solve and they
+   must be used with care to avoid combinatoric explosions *)
+
+Local Hint Resolve perm_swap perm_trans.
+Local Hint Resolve Permutation_sym Permutation_trans.
+
+(* This provides reflexivity, symmetry and transitivity and rewriting
+   on morphims to come *)
+
+Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
+  Equivalence_Reflexive := @Permutation_refl A ;
+  Equivalence_Symmetric := @Permutation_sym A ;
+  Equivalence_Transitive := @Permutation_trans A }.
+
+Instance Permutation_cons A :
+ Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.
+Proof.
+  repeat intro; subst; auto using perm_skip.
+Qed.
+
+Section Permutation_properties.
+
+Variable A:Type.
+
+Implicit Types a b : A.
+Implicit Types l m : list A.
+
+(** Compatibility with others operations on lists *)
+
+Theorem Permutation_in : forall (l l' : list A) (x : A),
+ Permutation l l' -> In x l -> In x l'.
+Proof.
+  intros l l' x Hperm; induction Hperm; simpl; tauto.
+Qed.
+
+Global Instance Permutation_in' :
+ Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.
+Proof.
+  repeat red; intros; subst; eauto using Permutation_in.
+Qed.
+
+Lemma Permutation_app_tail : forall (l l' tl : list A),
+ Permutation l l' -> Permutation (l++tl) (l'++tl).
+Proof.
+  intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
+  eapply Permutation_trans with (l':=l'++tl); trivial.
+Qed.
+
+Lemma Permutation_app_head : forall (l tl tl' : list A),
+ Permutation tl tl' -> Permutation (l++tl) (l++tl').
+Proof.
+  intros l tl tl' Hperm; induction l;
+   [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
+Qed.
+
+Theorem Permutation_app : forall (l m l' m' : list A),
+ Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
+Proof.
+  intros l m l' m' Hpermll' Hpermmm';
+   induction Hpermll' as [|x l l'|x y l|l l' l''];
+    repeat rewrite <- app_comm_cons; auto.
+  apply Permutation_trans with (l' := (x :: y :: l ++ m));
+   [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
+  apply Permutation_trans with (l' := (l' ++ m')); try assumption.
+  apply Permutation_app_tail; assumption.
+Qed.
+
+Global Instance Permutation_app' :
+ Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.
+Proof.
+  repeat intro; now apply Permutation_app.
+Qed.
+
+Lemma Permutation_add_inside : forall a (l l' tl tl' : list A),
+  Permutation l l' -> Permutation tl tl' ->
+  Permutation (l ++ a :: tl) (l' ++ a :: tl').
+Proof.
+  intros; apply Permutation_app; auto.
+Qed.
+
+Lemma Permutation_cons_append : forall (l : list A) x,
+  Permutation (x :: l) (l ++ x :: nil).
+Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
+Local Hint Resolve Permutation_cons_append.
+
+Theorem Permutation_app_comm : forall (l l' : list A),
+  Permutation (l ++ l') (l' ++ l).
+Proof.
+  induction l as [|x l]; simpl; intro l'.
+  rewrite app_nil_r; trivial. rewrite IHl.
+  rewrite app_comm_cons, Permutation_cons_append.
+  now rewrite <- app_assoc.
+Qed.
+Local Hint Resolve Permutation_app_comm.
+
+Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
+  Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
+Proof.
+  intros l l1 l2 a H. rewrite H.
+  rewrite app_comm_cons, Permutation_cons_append.
+  now rewrite <- app_assoc.
+Qed.
+Local Hint Resolve Permutation_cons_app.
+
+Theorem Permutation_middle : forall (l1 l2:list A) a,
+  Permutation (a :: l1 ++ l2) (l1 ++ a :: l2).
+Proof.
+  auto.
+Qed.
+Local Hint Resolve Permutation_middle.
+
+Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
+Proof.
+  induction l as [| x l]; simpl; trivial. now rewrite IHl at 1.
+Qed.
+
+Global Instance Permutation_rev' :
+ Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.
+Proof.
+  repeat intro; now rewrite <- 2 Permutation_rev.
+Qed.
+
+Theorem Permutation_length : forall (l l' : list A),
+ Permutation l l' -> length l = length l'.
+Proof.
+  intros l l' Hperm; induction Hperm; simpl; auto. now transitivity (length l').
+Qed.
+
+Global Instance Permutation_length' :
+ Proper (@Permutation A ==> Logic.eq) (@length A) | 10.
+Proof.
+  exact Permutation_length.
+Qed.
+
+Theorem Permutation_ind_bis :
+ forall P : list A -> list A -> Prop,
+   P [] [] ->
+   (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
+   (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
+   (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
+   forall l l', Permutation l l' -> P l l'.
+Proof.
+  intros P Hnil Hskip Hswap Htrans.
+  induction 1; auto.
+  apply Htrans with (x::y::l); auto.
+  apply Hswap; auto.
+  induction l; auto.
+  apply Hskip; auto.
+  apply Hskip; auto.
+  induction l; auto.
+  eauto.
+Qed.
+
+Ltac break_list l x l' H :=
+  destruct l as [|x l']; simpl in *;
+  injection H; intros; subst; clear H.
+
+Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A),
+ ~ Permutation nil (l++x::l').
+Proof.
+  intros l l' x HF.
+  apply Permutation_nil in HF. destruct l; discriminate.
+Qed.
+
+Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
+  Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
+Proof.
+  intros l1 l2 l3 l4 a; revert l1 l2 l3 l4.
+  set (P l l' :=
+       forall l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 ->
+       Permutation (l1++l2) (l3++l4)).
+  cut (forall l l', Permutation l l' -> P l l').
+  intros H; intros; eapply H; eauto.
+  apply (Permutation_ind_bis P); unfold P; clear P.
+  - (* nil *)
+    intros; now destruct l1.
+  - (* skip *)
+    intros x l l' H IH; intros.
+    break_list l1 b l1' H0; break_list l3 c l3' H1.
+    auto.
+    now rewrite H.
+    now rewrite <- H.
+    now rewrite (IH _ _ _ _ eq_refl eq_refl).
+  - (* swap *)
+    intros x y l l' Hp IH; intros.
+    break_list l1 b l1' H; break_list l3 c l3' H0.
+    auto.
+    break_list l3' b l3'' H.
+    auto.
+    constructor. now rewrite Permutation_middle.
+    break_list l1' c l1'' H1.
+    auto.
+    constructor. now rewrite Permutation_middle.
+    break_list l3' d l3'' H; break_list l1' e l1'' H1.
+    auto.
+    rewrite perm_swap. constructor. now rewrite Permutation_middle.
+    rewrite perm_swap. constructor. now rewrite Permutation_middle.
+    now rewrite perm_swap, (IH _ _ _ _ eq_refl eq_refl).
+  - (*trans*)
+    intros.
+    destruct (In_split a l') as (l'1,(l'2,H6)).
+    rewrite <- H.
+    subst l.
+    apply in_or_app; right; red; auto.
+    apply perm_trans with (l'1++l'2).
+    apply (H0 _ _ _ _ H3 H6).
+    apply (H2 _ _ _ _ H6 H4).
+Qed.
+
+Theorem Permutation_cons_inv l l' a :
+ Permutation (a::l) (a::l') -> Permutation l l'.
+Proof.
+  intro H; exact (Permutation_app_inv [] l [] l' a H).
+Qed.
+
+Theorem Permutation_cons_app_inv l l1 l2 a :
+ Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
+Proof.
+  intro H; exact (Permutation_app_inv [] l l1 l2 a H).
+Qed.
+
+Theorem Permutation_app_inv_l : forall l l1 l2,
+ Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
+Proof.
+  induction l; simpl; auto.
+  intros.
+  apply IHl.
+  apply Permutation_cons_inv with a; auto.
+Qed.
+
+Theorem Permutation_app_inv_r : forall l l1 l2,
+ Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
+Proof.
+  induction l.
+  intros l1 l2; do 2 rewrite app_nil_r; auto.
+  intros.
+  apply IHl.
+  apply Permutation_app_inv with a; auto.
+Qed.
+
+Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
+Proof.
+  intros a l H; remember [a] as m in H.
+  induction H; try (injection Heqm as -> ->; clear Heqm);
+    discriminate || auto.
+  apply Permutation_nil in H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
+Proof.
+  intros a b H.
+  apply Permutation_length_1_inv in H; injection H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_2_inv :
+  forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].
+Proof.
+  intros a1 a2 l H; remember [a1;a2] as m in H.
+  revert a1 a2 Heqm.
+  induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
+    discriminate || (try tauto).
+  apply Permutation_length_1_inv in H as ->; left; auto.
+  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
+    auto.
+Qed.
+
+Lemma Permutation_length_2 :
+  forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] ->
+    a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
+Proof.
+  intros a1 b1 a2 b2 H.
+  apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
+Qed.
+
+Let in_middle l l1 l2 (a:A) : l = l1 ++ a :: l2 ->
+ forall x, In x l <-> a = x \/ In x (l1++l2).
+Proof.
+ intros; subst; rewrite !in_app_iff; simpl. tauto.
+Qed.
+
+Lemma NoDup_cardinal_incl (l l' : list A) : NoDup l -> NoDup l' ->
+  length l = length l' -> incl l l' -> incl l' l.
+Proof.
+ intros N. revert l'. induction N as [|a l Hal Hl IH].
+ - destruct l'; now auto.
+ - intros l' Hl' E H x Hx.
+   assert (Ha : In a l') by (apply H; simpl; auto).
+   destruct (in_split _ _ Ha) as (l1 & l2 & H12). clear Ha.
+   rewrite in_middle in Hx; eauto.
+   destruct Hx as [Hx|Hx]; [left|right]; auto.
+   apply (IH (l1++l2)); auto.
+   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
+   * apply eq_add_S.
+     simpl in E; rewrite E, H12, !app_length; simpl; auto with arith.
+   * intros y Hy. assert (Hy' : In y l') by (apply H; simpl; auto).
+     rewrite in_middle in Hy'; eauto.
+     destruct Hy'; auto. subst y; intuition.
+Qed.
+
+Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' ->
+  (forall x:A, In x l <-> In x l') -> Permutation l l'.
+Proof.
+ intros N. revert l'. induction N as [|a l Hal Hl IH].
+ - destruct l'; simpl; auto.
+   intros Hl' H. exfalso. rewrite (H a); auto.
+ - intros l' Hl' H.
+   assert (Ha : In a l') by (apply H; simpl; auto).
+   destruct (In_split _ _ Ha) as (l1 & l2 & H12).
+   rewrite H12.
+   apply Permutation_cons_app.
+   apply IH; auto.
+   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
+   * intro x. split; intros Hx.
+     + assert (Hx' : In x l') by (apply H; simpl; auto).
+       rewrite in_middle in Hx'; eauto.
+       destruct Hx'; auto. subst; intuition.
+     + assert (Hx' : In x l') by (rewrite (in_middle l1 l2 a); eauto).
+       rewrite <- H in Hx'. destruct Hx'; auto.
+       subst. destruct (NoDup_remove_2 _ _ _ Hl' Hx).
+Qed.
+
+Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' ->
+  length l = length l' -> incl l l' -> Permutation l l'.
+Proof.
+ intros. apply NoDup_Permutation; auto.
+ split; auto. apply NoDup_cardinal_incl; auto.
+Qed.
+
+Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.
+Proof.
+ induction 1; auto.
+ * inversion_clear 1; constructor; eauto using Permutation_in.
+ * inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *.
+   constructor. simpl; intuition. constructor; intuition.
+Qed.
+
+Global Instance Permutation_NoDup' :
+ Proper (@Permutation A ==> iff) (@NoDup A) | 10.
+Proof.
+  repeat red; eauto using Permutation_NoDup.
+Qed.
+
+End Permutation_properties.
+
+Section Permutation_map.
+
+Variable A B : Type.
+Variable f : A -> B.
+
+Lemma Permutation_map l l' :
+  Permutation l l' -> Permutation (map f l) (map f l').
+Proof.
+ induction 1; simpl; eauto.
+Qed.
+
+Global Instance Permutation_map' :
+  Proper (@Permutation A ==> @Permutation B) (map f) | 10.
+Proof.
+  exact Permutation_map.
+Qed.
+
+End Permutation_map.
+
+Section Injection.
+
+Definition injective {A B} (f : A->B) :=
+ forall x y, f x = f y -> x = y.
+
+Lemma injective_map_NoDup {A B} (f:A->B) (l:list A) :
+ injective f -> NoDup l -> NoDup (map f l).
+Proof.
+ intros Hf. induction 1 as [|x l Hx Hl IH]; simpl; constructor; trivial.
+ rewrite in_map_iff. intros (y & Hy & Hy'). apply Hf in Hy. now subst.
+Qed.
+
+Lemma injective_bounded_surjective n f :
+ injective f ->
+ (forall x, x < n -> f x < n) ->
+ (forall y, y < n -> exists x, x < n /\ f x = y).
+Proof.
+ intros Hf H.
+ set (l := seq 0 n).
+ assert (P : incl (map f l) l).
+ { intros x. rewrite in_map_iff. intros (y & <- & Hy').
+   unfold l in *. rewrite in_seq in *. simpl in *.
+   destruct Hy' as (_,Hy'). auto with arith. }
+ assert (P' : incl l (map f l)).
+ { unfold l.
+   apply NoDup_cardinal_incl; auto using injective_map_NoDup, seq_NoDup.
+   now rewrite map_length. }
+ intros x Hx.
+ assert (Hx' : In x l) by (unfold l; rewrite in_seq; auto with arith).
+ apply P' in Hx'.
+ rewrite in_map_iff in Hx'. destruct Hx' as (y & Hy & Hy').
+ exists y; split; auto. unfold l in *; rewrite in_seq in Hy'.
+ destruct Hy'; auto with arith.
+Qed.
+
+Lemma nat_bijection_Permutation n f :
+ injective f -> (forall x, x < n -> f x < n) ->
+ let l := seq 0 n in Permutation (map f l) l.
+Proof.
+ intros Hf BD.
+ apply NoDup_Permutation_bis; auto using injective_map_NoDup, seq_NoDup.
+ * now rewrite map_length.
+ * intros x. rewrite in_map_iff. intros (y & <- & Hy').
+   rewrite in_seq in *. simpl in *.
+   destruct Hy' as (_,Hy'). auto with arith.
+Qed.
+
+End Injection.
+
+Section Permutation_alt.
+Variable A:Type.
+Implicit Type a : A.
+Implicit Type l : list A.
+
+(** Alternative characterization of permutation
+    via [nth_error] and [nth] *)
+
+Let adapt f n :=
+ let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.
+
+Let adapt_injective f : injective f -> injective (adapt f).
+Proof.
+ unfold adapt. intros Hf x y EQ.
+ destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT'].
+ - now apply eq_add_S, Hf.
+ - apply Lt.le_lt_or_eq in LE.
+   destruct LE as [LT|EQ']; [|now apply Hf in EQ'].
+   unfold lt in LT. rewrite EQ in LT.
+   rewrite <- (Lt.S_pred _ _ LT') in LT.
+   elim (Lt.lt_not_le _ _ LT' LT).
+ - apply Lt.le_lt_or_eq in LE'.
+   destruct LE' as [LT'|EQ']; [|now apply Hf in EQ'].
+   unfold lt in LT'. rewrite <- EQ in LT'.
+   rewrite <- (Lt.S_pred _ _ LT) in LT'.
+   elim (Lt.lt_not_le _ _ LT LT').
+ - apply eq_add_S, Hf.
+   now rewrite (Lt.S_pred _ _ LT), (Lt.S_pred _ _ LT'), EQ.
+Qed.
+
+Let adapt_ok a l1 l2 f : injective f -> length l1 = f 0 ->
+ forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n).
+Proof.
+ unfold adapt. intros Hf E n.
+ destruct le_lt_dec as [LE|LT].
+ - apply Lt.le_lt_or_eq in LE.
+   destruct LE as [LT|EQ]; [|now apply Hf in EQ].
+   rewrite <- E in LT.
+   rewrite 2 nth_error_app1; auto.
+ - rewrite (Lt.S_pred _ _ LT) at 1.
+   rewrite <- E, (Lt.S_pred _ _ LT) in LT.
+   rewrite 2 nth_error_app2; auto with arith.
+   rewrite <- Minus.minus_Sn_m; auto with arith.
+Qed.
+
+Lemma Permutation_nth_error l l' :
+ Permutation l l' <->
+  (length l = length l' /\
+   exists f:nat->nat,
+    injective f /\ forall n, nth_error l' n = nth_error l (f n)).
+Proof.
+ split.
+ { intros P.
+   split; [now apply Permutation_length|].
+   induction P.
+   - exists (fun n => n).
+     split; try red; auto.
+   - destruct IHP as (f & Hf & Hf').
+     exists (fun n => match n with O => O | S n => S (f n) end).
+     split; try red.
+     * intros [|y] [|z]; simpl; now auto.
+     * intros [|n]; simpl; auto.
+   - exists (fun n => match n with 0 => 1 | 1 => 0 | n => n end).
+     split; try red.
+     * intros [|[|z]] [|[|t]]; simpl; now auto.
+     * intros [|[|n]]; simpl; auto.
+   - destruct IHP1 as (f & Hf & Hf').
+     destruct IHP2 as (g & Hg & Hg').
+     exists (fun n => f (g n)).
+     split; try red.
+     * auto.
+     * intros n. rewrite <- Hf'; auto. }
+ { revert l. induction l'.
+   - intros [|l] (E & _); now auto.
+   - intros l (E & f & Hf & Hf').
+     simpl in E.
+     assert (Ha : nth_error l (f 0) = Some a)
+      by (symmetry; apply (Hf' 0)).
+     destruct (nth_error_split l (f 0) Ha) as (l1 & l2 & L12 & L1).
+     rewrite L12. rewrite <- Permutation_middle. constructor.
+     apply IHl'; split; [|exists (adapt f); split].
+     * revert E. rewrite L12, !app_length. simpl.
+       rewrite <- plus_n_Sm. now injection 1.
+     * now apply adapt_injective.
+     * intro n. rewrite <- (adapt_ok a), <- L12; auto.
+       apply (Hf' (S n)). }
+Qed.
+
+Lemma Permutation_nth_error_bis l l' :
+ Permutation l l' <->
+  exists f:nat->nat,
+    injective f /\
+    (forall n, n < length l -> f n < length l) /\
+    (forall n, nth_error l' n = nth_error l (f n)).
+Proof.
+ rewrite Permutation_nth_error; split.
+ - intros (E & f & Hf & Hf').
+   exists f. do 2 (split; trivial).
+   intros n Hn.
+   destruct (Lt.le_or_lt (length l) (f n)) as [LE|LT]; trivial.
+   rewrite <- nth_error_None, <- Hf', nth_error_None, <- E in LE.
+   elim (Lt.lt_not_le _ _ Hn LE).
+ - intros (f & Hf & Hf2 & Hf3); split; [|exists f; auto].
+   assert (H : length l' <= length l') by auto with arith.
+   rewrite <- nth_error_None, Hf3, nth_error_None in H.
+   destruct (Lt.le_or_lt (length l) (length l')) as [LE|LT];
+    [|apply Hf2 in LT; elim (Lt.lt_not_le _ _ LT H)].
+   apply Lt.le_lt_or_eq in LE. destruct LE as [LT|EQ]; trivial.
+   rewrite <- nth_error_Some, Hf3, nth_error_Some in LT.
+   destruct (injective_bounded_surjective Hf Hf2 LT) as (y & Hy & Hy').
+   apply Hf in Hy'. subst y. elim (Lt.lt_irrefl _ Hy).
+Qed.
+
+Lemma Permutation_nth l l' d :
+ Permutation l l' <->
+  (let n := length l in
+   length l' = n /\
+   exists f:nat->nat,
+    (forall x, x < n -> f x < n) /\
+    (forall x y, x < n -> y < n -> f x = f y -> x = y) /\
+    (forall x, x < n -> nth x l' d = nth (f x) l d)).
+Proof.
+ split.
+ - intros H.
+   assert (E := Permutation_length H).
+   split; auto.
+   apply Permutation_nth_error_bis in H.
+   destruct H as (f & Hf & Hf2 & Hf3).
+   exists f. split; [|split]; auto.
+   intros n Hn. rewrite <- 2 nth_default_eq. unfold nth_default.
+    now rewrite Hf3.
+ - intros (E & f & Hf1 & Hf2 & Hf3).
+   rewrite Permutation_nth_error.
+   split; auto.
+   exists (fun n => if le_lt_dec (length l) n then n else f n).
+   split.
+   * intros x y.
+     destruct le_lt_dec as [LE|LT];
+      destruct le_lt_dec as [LE'|LT']; auto.
+     + apply Hf1 in LT'. intros ->.
+       elim (Lt.lt_irrefl (f y)). eapply Lt.lt_le_trans; eauto.
+     + apply Hf1 in LT. intros <-.
+       elim (Lt.lt_irrefl (f x)). eapply Lt.lt_le_trans; eauto.
+   * intros n.
+     destruct le_lt_dec as [LE|LT].
+     + assert (LE' : length l' <= n) by (now rewrite E).
+       rewrite <- nth_error_None in LE, LE'. congruence.
+     + assert (LT' : n < length l') by (now rewrite E).
+       specialize (Hf3 n LT). rewrite <- 2 nth_default_eq in Hf3.
+       unfold nth_default in Hf3.
+       apply Hf1 in LT.
+       rewrite <- nth_error_Some in LT, LT'.
+       do 2 destruct nth_error; congruence.
+Qed.
+
+End Permutation_alt.
+
+(* begin hide *)
+Notation Permutation_app_swap := Permutation_app_comm (only parsing).
+(* end hide *)

samples/Coq/Poly.v

@@ -0,0 +1,875 @@
+Require Export Lists.
+Require Export Basics.
+
+Import Playground1.
+
+Inductive list (X : Type) : Type :=
+	| nil : list X
+	| cons : X -> list X -> list X.
+
+Fixpoint length (X:Type) (l:list X) : nat :=
+	match l with
+		| nil => O
+		| cons h t => S (length X t)
+	end.
+
+Fixpoint app (X : Type) (l1 l2 : list X)
+										: (list X) :=
+	match l1 with
+		| nil => l2
+		| cons h t => cons X h (app X t l2)
+	end.
+
+Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
+	match l with
+		| nil => cons X v (nil X)
+		| cons h t => cons X h (snoc X t v)
+	end.
+
+Fixpoint rev (X:Type) (l:list X) : list X :=
+	match l with
+		| nil => nil X
+		| cons h t => snoc X (rev X t) h
+	end.
+
+
+Implicit Arguments nil [[X]].
+Implicit Arguments cons [[X]].
+Implicit Arguments length [[X]].
+Implicit Arguments app [[X]].
+Implicit Arguments rev [[X]].
+Implicit Arguments snoc [[X]].
+
+Definition list123 := cons 1 (cons 2 (cons 3 (nil))).
+
+Notation "x :: y" := (cons x y) (at level 60, right associativity).
+Notation "[]" := nil.
+Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
+Notation "x ++ y" := (app x y) (at level 60, right associativity).
+
+Fixpoint repeat (X : Type) (n : X) (count : nat) : list X :=
+	match count with
+		| O => nil
+		| S count' => n :: (repeat _ n count')
+	end.
+
+Example test_repeat1:
+	repeat bool true (S (S O)) = [true, true].
+Proof. reflexivity. Qed.
+
+Theorem nil_app : forall X:Type, forall l:list X,
+	app [] l = l.
+Proof.
+	reflexivity.
+	Qed.
+
+Theorem rev_snoc : forall X : Type,
+									 forall v : X,
+									 forall s : list X,
+	rev (snoc s v) = v :: (rev s).
+Proof.
+	intros X v s.
+	induction s.
+		reflexivity.
+		simpl.
+		rewrite -> IHs.
+		reflexivity.
+		Qed.
+
+Theorem snoc_with_append : forall X : Type,
+													 forall l1 l2 : list X,
+													 forall v : X,
+	snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
+Proof.
+	intros X l1 l2 v.
+	induction l1.
+		reflexivity.
+		simpl.
+		rewrite -> IHl1.
+		reflexivity.
+		Qed.
+
+Inductive prod (X Y : Type) : Type :=
+	pair : X -> Y -> prod X Y.
+
+Implicit Arguments pair [X Y].
+
+Notation "( x , y )" := (pair x y).
+Notation "X * Y" := (prod X Y) : type_scope.
+
+Definition fst (X Y : Type) (p : X * Y) : X :=
+	match p with (x,y) => x end.
+Definition snd (X Y : Type) (p : X * Y) : Y :=
+	match p with (x,y) => y end.
+
+Fixpoint combine (X Y : Type) (lx : list X) (ly : list Y)
+			: list (X * Y) :=
+	match lx, ly with
+		| [], _ => []
+		| _,[] => []
+		| x::tx, y::ty => (x,y) :: (combine _ _ tx ty)
+	end.
+
+Implicit Arguments combine [X Y].
+
+Fixpoint split {X Y: Type} (s : list (X * Y)) : (list X)*(list Y) :=
+	match s with
+		| nil => (nil, nil)
+		| (x,y) :: tp => match split tp with
+											| (lx, ly) => (x :: lx, y :: ly)
+										 end
+	end.
+
+Inductive option (X : Type) : Type :=
+	| Some : X -> option X
+	| None : option X.
+
+Implicit Arguments Some [X].
+Implicit Arguments None [X].
+
+Fixpoint index (X : Type) (n : nat)
+							 (l : list X) : option X :=
+	match n with
+		| O => match l with
+								| nil => None
+								| x :: xs => Some x
+					 end
+		| S n' => match l with
+									| nil => None
+									| x :: xs => index X n' xs
+							end
+	end.
+
+Definition hd_opt (X : Type) (l : list X) : option X :=
+		match l with
+			| nil => None
+			| x :: xs => Some x
+		end.
+
+Implicit Arguments hd_opt [X].
+
+Example test_hd_opt1 : hd_opt [S O, S (S O)] = Some (S O).
+Proof. reflexivity. Qed.
+Example test_hd_opt2 : hd_opt [[S O], [S (S O)]] = Some [S O].
+Proof. reflexivity. Qed.
+
+Definition plus3 := plus (S (S (S O))).
+
+Definition prod_curry {X Y Z : Type}
+		(f : X * Y -> Z) (x : X) (y : Y) : Z := f (x,y).
+
+Definition prod_uncurry {X Y Z : Type}
+	(f : X -> Y -> Z) (p : X * Y) : Z :=
+	f (fst X Y p) (snd X Y p).
+
+Theorem uncurry_uncurry : forall (X Y Z : Type) (f : X -> Y -> Z) x y,
+				prod_curry (prod_uncurry f) x y = f x y.
+Proof.
+	reflexivity.
+Qed.
+
+Theorem curry_uncurry : forall (X Y Z : Type) (f : (X * Y) -> Z)
+	(p : X * Y),
+		prod_uncurry (prod_curry f) p = f p.
+Proof.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Fixpoint filter (X : Type) (test : X -> bool) (l:list X)
+				: (list X) :=
+		match l with
+			| [] => []
+		  | h :: t => if test h then h :: (filter _ test t)
+									else filter _ test t
+		end.
+
+Definition countoddmembers' (l:list nat) : nat :=
+	length (filter _ oddb l).
+
+Definition partition (X : Type) (test : X -> bool) (l : list X)
+							: list X * list X :=
+	(filter _ test l, filter _ (fun el => negb (test el)) l).
+
+Example test_partition1: partition _ oddb [S O, S (S O), S (S (S O)), S (S (S (S O))), S (S (S (S (S O))))] = ([S O, S (S (S O)), S (S (S (S (S O))))], [S (S O), S (S (S (S O)))]).
+Proof. reflexivity. Qed.
+
+Fixpoint map {X Y : Type} (f : X -> Y) (l : list X) : (list Y ) :=
+		match l with
+			| [] => []
+			| h :: t => (f h) :: (map f t)
+		end.
+
+Example test_map1: map (plus (S (S (S O)))) [S (S O), O, S (S O)] = [S (S (S (S (S O)))), S (S (S O)), S (S (S (S (S O))))].
+Proof. reflexivity. Qed.
+
+ Theorem map_rev_1 : forall (X Y: Type) (f: X -> Y) (l : list X) (x : X),
+ 		map f (snoc l x) = snoc (map f l) (f x).
+Proof.
+	intros X Y f l x.
+	induction l.
+	reflexivity.
+	simpl.
+	rewrite -> IHl.
+	reflexivity.
+	Qed.
+
+Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
+				map f (rev l) = rev (map f l).
+Proof.
+	intros X Y f l.
+	induction l.
+		reflexivity.
+		simpl.
+		rewrite <- IHl.
+		rewrite -> map_rev_1.
+		reflexivity.
+		Qed.
+
+Fixpoint flat_map {X Y : Type} (f : X -> list Y) (l : list X)
+			: (list Y) :=
+	match l with
+		| [] => []
+		| x :: xs => (f x) ++ (flat_map f xs)
+	end.
+
+Definition map_option {X Y : Type} (f : X -> Y) (xo : option X)
+		: option Y :=
+	match xo with
+		| None => None
+		| Some x => Some (f x)
+	end.
+
+Fixpoint fold {X Y: Type} (f: X -> Y -> Y) (l:list X) (b:Y) : Y :=
+	match l with
+		| nil => b
+		| h :: t => f h (fold f t b)
+	end.
+
+Example fold_example : fold andb [true, true, false, true] true = false.
+Proof. reflexivity. Qed.
+
+Definition constfun {X : Type} (x: X) : nat -> X :=
+	fun (k:nat) => x.
+
+Definition ftrue := constfun true.
+Example constfun_example : ftrue O = true.
+Proof. reflexivity. Qed.
+
+Definition override {X : Type} (f: nat -> X) (k:nat) (x:X) : nat->X :=
+	fun (k':nat) => if beq_nat k k' then x else f k'.
+
+Definition fmostlytrue := override (override ftrue (S O) false) (S (S (S O))) false.
+
+Example override_example1 : fmostlytrue O = true.
+Proof. reflexivity. Qed.
+Example override_example2 : fmostlytrue (S O) = false.
+Proof. reflexivity. Qed.
+Example override_example3 : fmostlytrue (S (S O)) = true.
+Proof. reflexivity. Qed.
+Example override_example4 : fmostlytrue (S (S (S O))) = false.
+Proof. reflexivity. Qed.
+
+Theorem override_example : forall (b: bool),
+	(override (constfun b) (S (S (S O))) true) (S (S O)) = b.
+Proof.
+	reflexivity.
+Qed.
+
+Theorem unfold_example_bad : forall m n,
+	(S (S (S O))) + n = m ->
+	plus3 n = m.
+Proof.
+	intros m n H.
+	unfold plus3.
+	rewrite -> H.
+	reflexivity.
+	Qed.
+
+Theorem override_eq : forall {X : Type} x k (f : nat -> X),
+	(override f k x) k = x.
+Proof.
+	intros X x k f.
+	unfold override.
+	rewrite <- beq_nat_refl.
+	reflexivity.
+	Qed.
+
+Theorem override_neq : forall {X : Type} x1 x2 k1 k2 (f : nat->X),
+	f k1 = x1 ->
+		beq_nat k2 k1 = false ->
+			(override f k2 x2) k1 = x1.
+Proof.
+	intros X x1 x2 k1 k2 f eq1 eq2.
+	unfold override.
+	rewrite -> eq2.
+	rewrite -> eq1.
+	reflexivity.
+Qed.
+
+Theorem eq_add_S : forall (n m : nat),
+	S n = S m ->
+		n = m.
+Proof.
+	intros n m eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem silly4 : forall (n m : nat),
+	[n] = [m] ->
+		n = m.
+Proof.
+	intros n o eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem silly5 : forall (n m o : nat),
+	[n,m] = [o,o] ->
+		[n] = [m].
+Proof.
+	intros n m o eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem sillyex1 : forall (X : Type) (x y z : X) (l j : list X),
+	x :: y :: l = z :: j ->
+		y :: l = x :: j ->
+			x = y.
+Proof.
+	intros X x y z l j.
+	intros eq1 eq2.
+	inversion eq1.
+	inversion eq2.
+	symmetry.
+	rewrite -> H0.
+	reflexivity.
+Qed.
+
+Theorem silly6 : forall (n : nat),
+	S n = O ->
+		(S (S O)) + (S (S O)) = (S (S (S (S (S O))))).
+Proof.
+	intros n contra.
+	inversion contra.
+Qed.
+
+Theorem silly7 : forall (n m : nat),
+				false = true ->
+					[n] = [m].
+Proof.
+	intros n m contra.
+	inversion contra.
+Qed.
+
+Theorem sillyex2 : forall (X : Type) (x y z : X) (l j : list X),
+	x :: y :: l = [] ->
+		y :: l = z :: j ->
+			x = z.
+Proof.
+	intros X x y z l j contra.
+	inversion contra.
+	Qed.
+
+Theorem beq_nat_eq : forall n m,
+	true = beq_nat n m -> n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		intros m. destruct m as [| m'].
+		SCase "m = 0". reflexivity.
+		SCase "m = S m'". simpl. intros contra. inversion contra.
+	Case "n = S n'".
+		intros m. destruct m as [| m'].
+		SCase "m = 0". simpl. intros contra. inversion contra.
+		SCase "m = S m'". simpl. intros H.
+			assert(n' = m') as Hl.
+				SSCase "Proof of assertion". apply IHn'. apply H.
+			rewrite -> Hl. reflexivity.
+Qed.
+
+Theorem beq_nat_eq' : forall m n,
+				beq_nat n m = true -> n = m.
+Proof.
+	intros m. induction m as [| m'].
+	Case "m = O".
+		destruct n.
+		SCase "n = O".
+			reflexivity.
+		SCase "n = S n'".
+			simpl. intros contra. inversion contra.
+	Case "m = S m'".
+		simpl.
+		destruct n.
+		SCase "n = O".
+			simpl. intros contra. inversion contra.
+		SCase "n = S n'".
+			simpl. intros H.
+			assert (n = m') as Hl.
+				apply IHm'.
+				apply H.
+			rewrite -> Hl.
+			reflexivity.
+Qed.
+
+Theorem length_snoc' : forall (X : Type) (v : X)
+(l : list X) (n : nat),
+	length l = n ->
+	length (snoc l v) = S n.
+	Proof.
+	intros X v l. induction l as [| v' l'].
+	Case "l = []". intros n eq. rewrite <- eq. reflexivity.
+	Case "l = v' :: l'". intros n eq. simpl. destruct n as [| n'].
+	SCase "n = 0". inversion eq.
+	SCase "n = S n'".
+	assert (length (snoc l' v) = S n').
+	SSCase "Proof of assertion". apply IHl'.
+	inversion eq. reflexivity.
+	rewrite -> H. reflexivity.
+	Qed.
+
+	Theorem beq_nat_O_l : forall n,
+	true = beq_nat O n -> O = n.
+	Proof.
+	intros n. destruct n.
+	reflexivity.
+	simpl.
+	intros contra.
+	inversion contra.
+	Qed.
+
+Theorem beq_nat_O_r : forall n,
+	true = beq_nat n O -> O = n.
+Proof.
+	intros n.
+	induction n.
+	Case "n = O".
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		intros contra.
+		inversion contra.
+	Qed.
+
+Theorem double_injective : forall n m,
+	double n = double m ->
+		n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		simpl. intros m eq.
+		destruct m as [|m'].
+		SCase "m = O". reflexivity.
+		SCase "m = S m'". inversion eq.
+	Case "n = S n'". intros m eq. destruct m as [| m'].
+		SCase "m = O". inversion eq.
+		SCase "m = S m'".
+			assert(n' = m') as H.
+				SSCase "Proof of assertion". apply IHn'. inversion eq. reflexivity.
+			rewrite -> H. reflexivity.
+Qed.
+
+Theorem silly3' : forall (n : nat),
+	(beq_nat n (S (S (S (S (S O))))) = true ->
+	 	beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))) = true) ->
+		true = beq_nat n (S (S (S (S (S O))))) ->
+			true = beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))).
+Proof.
+	intros n eq H.
+	symmetry in H.
+	apply eq in H.
+	symmetry in H.
+	apply H.
+Qed.
+
+Theorem plus_n_n_injective : forall n m,
+					n + n = m + m ->
+						n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		simpl. intros m.
+		destruct m.
+			SCase "m = O".
+			reflexivity.
+			SCase "m = S m'".
+			simpl.
+			intros contra.
+			inversion contra.
+	Case "n = S n".
+		intros m.
+		destruct m.
+			SCase "m = O".
+			intros contra.
+			inversion contra.
+			SCase "m = S m'".
+			intros eq.
+			inversion eq.
+			rewrite <- plus_n_Sm in H0.
+			rewrite <- plus_n_Sm in H0.
+			inversion H0.
+			apply IHn' in H1.
+			rewrite -> H1.
+			reflexivity.
+	Qed.
+
+Theorem override_shadow : forall {X : Type} x1 x2 k1 k2 (f : nat -> X),
+	(override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.
+Proof.
+	intros X x1 x2 k1 k2 f.
+	unfold override.
+	destruct (beq_nat k1 k2).
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem combine_split : forall (X : Type) (Y : Type) (l : list (X * Y)) (l1: list X) (l2: list Y),
+				split l = (l1, l2) -> combine l1 l2 = l.
+Proof.
+	intros X Y l.
+	induction l as [| x y].
+	Case "l = nil".
+		intros l1 l2.
+		intros eq.
+		simpl.
+		simpl in eq.
+		inversion eq.
+		reflexivity.
+	Case "l = ::".
+		intros l1 l2.
+		simpl.
+		destruct x.
+		destruct (split y).
+		simpl.
+		destruct l1.
+		SCase "l1 = []".
+			simpl.
+			induction l2.
+			SSCase "l2 = []".
+				intros contra.
+				inversion contra.
+			SSCase "l2 = ::".
+				intros contra.
+				inversion contra.
+		SCase "l1 = ::".
+			induction l2.
+			SSCase "l2 = []".
+				simpl.
+				intros contra.
+				inversion contra.
+			SSCase "l2 = ::".
+				simpl.
+				intros eq.
+				inversion eq.
+				simpl.
+				rewrite IHy.
+				reflexivity.
+				simpl.
+				rewrite H1.
+				rewrite H3.
+				reflexivity.
+Qed.
+
+Theorem split_combine : forall (X : Type) (Y : Type) (l1: list X) (l2: list Y),
+				length l1 = length l2 -> split (combine l1 l2) = (l1, l2).
+Proof.
+intros X Y.
+intros l1.
+induction l1.
+simpl.
+intros l2.
+induction l2.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct l2.
+simpl.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+inversion eq.
+apply IHl1 in H0.
+rewrite H0.
+reflexivity.
+Qed.
+
+Definition sillyfun1 (n : nat) : bool :=
+	 if beq_nat n (S (S (S O))) then true
+	 else if beq_nat n (S (S (S (S (S O))))) then true
+				else false.
+
+Theorem beq_equal : forall (a b : nat),
+		beq_nat a b = true ->
+			a = b.
+Proof.
+intros a.
+induction a.
+destruct b.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct b.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+apply IHa in eq.
+rewrite eq.
+reflexivity.
+Qed.
+
+Theorem override_same : forall {X : Type} x1 k1 k2 (f : nat->X),
+	f k1 = x1 ->
+		(override f k1 x1) k2 = f k2.
+Proof.
+	intros X x1 k1 k2 f eq.
+	unfold override.
+	remember (beq_nat k1 k2) as a.
+	destruct a.
+	rewrite <- eq.
+	symmetry in Heqa.
+	apply beq_equal in Heqa.
+	rewrite -> Heqa.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+
+Theorem filter_exercise : forall (X : Type) (test : X -> bool)
+	(x : X) (l lf : list X),
+	filter _ test l = x :: lf ->
+		test x = true.
+Proof.
+intros X.
+intros test.
+intros x.
+induction l.
+simpl.
+intros lf.
+intros contra.
+inversion contra.
+
+simpl.
+remember (test x0) as a.
+destruct a.
+simpl.
+intros lf.
+intros eq.
+rewrite Heqa.
+inversion eq.
+reflexivity.
+
+intros lf.
+intros eq.
+apply IHl in eq.
+rewrite eq.
+reflexivity.
+Qed.
+
+Theorem trans_eq : forall {X:Type} (n m o : X),
+				n = m -> m = o -> n = o.
+Proof.
+	intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2.
+	reflexivity.
+Qed.
+
+Example trans_eq_example' : forall (a b c d e f : nat),
+				[a,b] = [c,d] ->
+				[c,d] = [e,f] ->
+				[a,b] = [e,f].
+Proof.
+	intros a b c d e f eq1 eq2.
+	apply trans_eq with (m := [c,d]). apply eq1. apply eq2.
+	Qed.
+
+Theorem trans_eq_exercise : forall (n m o p : nat),
+		m = (minustwo o) ->
+		(n + p) = m ->
+		(n + p) = (minustwo o).
+Proof.
+intros n m o p.
+intros eq1 eq2.
+rewrite eq2.
+rewrite <- eq1.
+reflexivity.
+Qed.
+
+Theorem beq_nat_trans : forall n m p,
+				true = beq_nat n m ->
+				true = beq_nat m p ->
+				true = beq_nat n p.
+Proof.
+intros n m p.
+intros eq1 eq2.
+symmetry  in eq1.
+symmetry  in eq2.
+apply beq_equal in eq1.
+apply beq_equal in eq2.
+rewrite eq1.
+rewrite <- eq2.
+apply beq_nat_refl.
+Qed.
+
+Theorem override_permute : forall {X:Type} x1 x2 k1 k2 k3 (f : nat->X),
+	false = beq_nat k2 k1 ->
+	(override (override f k2 x2) k1 x1) k3 = (override (override f k1 x1) k2 x2) k3.
+Proof.
+intros X x1 x2 k1 k2 k3 f.
+simpl.
+unfold override.
+remember (beq_nat k1 k3).
+remember (beq_nat k2 k3).
+destruct b.
+destruct b0.
+symmetry  in Heqb.
+symmetry  in Heqb0.
+apply beq_equal in Heqb.
+apply beq_equal in Heqb0.
+rewrite <- Heqb in Heqb0.
+assert (k2 = k1 -> true = beq_nat k2 k1).
+destruct k2.
+destruct k1.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct k1.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+inversion eq.
+symmetry .
+symmetry .
+apply beq_nat_refl.
+
+apply H in Heqb0.
+rewrite <- Heqb0.
+intros contra.
+inversion contra.
+
+intros eq.
+reflexivity.
+
+destruct b0.
+intros eq.
+reflexivity.
+
+intros eq.
+reflexivity.
+
+Qed.
+
+Definition fold_length {X : Type} (l : list X) : nat :=
+	fold (fun _ n => S n) l O.
+
+Example test_fold_length1 : fold_length [S (S (S (S O))), S (S (S (S (S (S (S O)))))), O] = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Theorem fold_length_correct : forall X (l :list X),
+	fold_length l = length l.
+Proof.
+	intros X l.
+	unfold fold_length.
+	induction l.
+	Case "l = O".
+		reflexivity.
+	Case "l = ::".
+		simpl.
+		rewrite IHl.
+		reflexivity.
+	Qed.
+
+Definition fold_map {X Y: Type} (f : X -> Y) (l : list X) : list Y :=
+	fold (fun x total => (f x) :: total) l [].
+
+Theorem fold_map_correct : forall (X Y: Type) (f : X -> Y) (l : list X),
+	fold_map f l = map f l.
+Proof.
+	intros X Y f l.
+	unfold fold_map.
+	induction l.
+	reflexivity.
+	  
+	simpl.
+	rewrite IHl.
+	reflexivity.
+	Qed.
+
+Fixpoint forallb {X : Type} (f : X -> bool) (l : list X) :=
+	match l with
+		| nil => true
+		| x :: xs => andb (f x) (forallb f xs)
+	end.
+
+Fixpoint existsb {X : Type} (f : X -> bool) (l : list X) :=
+	match l with
+		| nil => false
+		| x :: xs => orb (f x) (existsb f xs)
+	end.
+
+Definition existsb2 {X : Type} (f: X -> bool) (l : list X) :=
+	negb (forallb (fun x => negb (f x)) l).
+
+Theorem existsb_correct : forall (X : Type) (f : X -> bool) (l : list X),
+		existsb f l = existsb2 f l.
+Proof.
+intros X f l.
+induction l.
+reflexivity.
+
+simpl.
+rewrite IHl.
+unfold existsb2.
+simpl.
+destruct (forallb (fun x0 : X => negb (f x0)) l).
+simpl.
+destruct (f x).
+reflexivity.
+
+reflexivity.
+
+destruct (f x).
+reflexivity.
+
+reflexivity.
+
+Qed.
+
+Theorem index_okx : forall (X:Type) (l : list X) (n : nat),
+		length l = n -> index X (S n) l = None.
+Proof.
+	intros X l.
+	induction l.
+	reflexivity.
+
+	intros n.
+	destruct n.
+	intros contra.
+	inversion contra.
+
+	intros eq.
+	inversion eq.
+	apply IHl.
+	reflexivity.
+Qed.
+
+Inductive mumble : Type :=
+  | a : mumble
+	| b : mumble -> nat -> mumble
+	| c : mumble.
+Inductive grumble (X:Type) : Type :=
+ | d : mumble -> grumble X
+ | e : X -> grumble X.
+