checkprog.go

package main

import (
	"fmt"
)

func main() {
	s := []bool{false, false, false, false, false, false, false, false, false, false, false, false, false, false, false,
		true, true, true, true, true, true, true, true, true, true, true, true, true, true, true}

	end := []bool{true, true, true, true, true, true, true, true, true, true, true, true, true, true, true,
		false, false, false, false, false, false, false, false, false, false, false, false, false, false, false}

	cases := 0

	fmt.Println("start:")
	printSlice(s)

	for !equalSlices(s, end) {
		if !checkRequirement(s) {
			break
		}

		// change s to the next case

		encounteredOnes := 0
		j := 0
		stopLooping := false
		// we go through s
		for i := len(s) - 2; i >= 0 && !stopLooping; i-- {
			// count the number of ones we've encoutered
			if s[i+1] {
				encounteredOnes++
			}

			// if we find a 1 followed by a zero
			if s[i+1] && !s[i] {
				s[i] = true
				s[i+1] = false
				stopLooping = true

				// fill everything s[i-1] up to len(s)-encounteredOnes with zeroes
				for j = i + 2; j < len(s)-encounteredOnes+1; j++ {
					s[j] = false
				}
				// fill the remaining part with ones
				for ; j < len(s); j++ {
					s[j] = true
				}
			}
		}
		cases++
	}

	fmt.Println("\ns in the end:")
	printSlice(s)

	fmt.Println("\nNumber of cases tested:", cases)

	if theorem_is_true {
		fmt.Println("\nTheorem has been tested for all cases, and it's true.")
	} else {
		fmt.Println("\nWe have found a counterexample.")
	}
}

var theorem_is_true = true

func checkRequirement(s []bool) bool {
	numberTrue := 0
	numberFalse := 0

	i := 0
	// first part of slice
	for i = 0; i < 10; i++ {
		if s[i] {
			numberTrue++
		} else {
			numberFalse++
		}
	}

	for i = 10; i < len(s); i++ {
		if s[i] {
			numberTrue++
		} else {
			numberFalse++
		}

		if s[i-10] {
			numberTrue--
		} else {
			numberFalse--
		}

		if numberTrue == numberFalse {
			return true
		}
	}

	fmt.Println("\nRequirement not met, counterexample:")
	printSlice(s)
	theorem_is_true = false
	return false
}

func printSlice(s interface{}) {
	for _, v := range s.([]bool) {
		if v {
			fmt.Print("1")
		} else {
			fmt.Print("0")
		}
	}
	fmt.Print("\n")
}

func equalSlices(a, b []bool) bool {
	if len(a) != len(b) {
		return false
	}
	for i, v := range a {
		if v != b[i] {
			return false
		}
	}
	return true
}